iDaVer [an Integrated DAta model VERifier]

Overview

Most modern web applications are built using development frameworks based on the Model-View-Controller (MVC) pattern. In MVC-based web applications, the data model specifies the types of objects used by the application and the relations among them. Since the data model forms the foundation of such applications, its correctness is crucial. iDaVer is a tool that automatically performs data model verification for the MVC framework, Ruby on Rails.

iDaVer has two modes of operation. The first is automated verification of user-specified properties. Functionality includes:

Automatic extraction of a formal data model specification from applications implemented using the Ruby on Rails framework
Support of templates for specifying data model properties
Automatic translation of the properties specified using these templates to satisfiability queries in two different logics
Integrated support for using automated decision procedures (unbounded verification) and/or a SAT solver (bounded verification) to identify which properties are verified (i.e. satisfied by the data model)
Reporting counterexample instances for the properties that fail.

The other main mode of operation for iDaVer is automatic property inference and verification. This mode:

Automatically infers properties about the data model by analyzing the relations among the object classes and inferring three categories of properties.
Checks the inferred properties with respect to the semantics of the data model using automated verification techniques (unbounded verification, in particular).
For the properties that fail, repairs are generated that are suggested fixes of the data model that establish the inferred properties.

Overall, iDaVer enables automated verification of data models without requiring manually written formal specifications. In particular, usability is increased by combining automated data model extraction with template-based property specification and automated property inference.

Requirements

The requirements to run iDaVer include:

The data model of a Ruby on Rails 2.0 application (the "model" folder)
Ruby, version 1.9.3
The solver from MIT, Alloy Analyzer, version 4.1
Microsoft's SMT solver, Z3, version 2.4
Windows platform (for running Z3 and doing unbounded verification)

See further details in the README file.

Download Links

zip file
tarball

iDaVer Usage

iDaVer's basic usage is described below.

------------------------------------------------------------------------------
USAGE: ruby iDaVeR.rb [options] path\to\models\folder
  This program verifies the specified properties about a set of Ruby on Rails
  data models using the technique specified. (Bounded verification performed
  by default.) If no properties are specified using the -p option, automatic
  property inference is performed. Inferred properties are automatically
  verified using unbounded verification.

-p, --property FILENAME	Name of the file that contains the properties to verify
-u, --unbounded_verif	Performs unbounded (rather than bounded) verification using the SMT Solver, Z3
-b, --bound INT	Uses given bound rather than default of 20 (bounded verification only)
-j, --projection_on	Performs data model projection during verification (z3 only)
-c, --csv	Output verification stats as CSV. Default: false
-e, --erd [FILENAME]	Outputs entity-relation diagram (ERD) for given data model. Output as a .dot file unless user-specified FILENAME ends with .png.

------------------------------------------------------------------------------

Examples

For the examples below, we will use LovdByLess, an open-source, social networking application.

Example #1

To verify properties about the data model using our bounded verification approach, start by creating a text file with the list of properties you wish to check.

For example, we create a file called properties.txt. In it, we express the properties using templates (see our [FormaliSE'13] paper):

-----------------------------------------------
// properties.txt

deletePropagates[ Profile, Photo ]
alwaysRelated[ Photo, Profile ]
-----------------------------------------------

Next, we execute iDaVer to verify these properties using the command below.

>ruby iDaVer.rb -p properties.txt models\lovdbyless_models

Note that we input the properties to be verified using the -p option. The other required argument is the name of the directory containing the model files of the application. Runinng this command, we get the following output:

bounded_verif_sample_output

bounded_verif_sample_output2

iDaVer's output includes the verification technique chosen, the solver used, the size of the formula (SMT-LIB specification created by iDaVer) that was sent to the solver, the time taken by the solver to obtain a verification result, and . Finally, iDaVer outputs the result of the verification (whether the properties holds or does not hold on the data model), and provides a counterexample instance for properties that fail.

Example #2

To verify properties about the data using our unbounded verification approach, the steps are exactly the same as with bounded verification, except an additional command-line argument is provided to specify unbounded verification (-u).

>ruby iDaVer.rb -u -p properties.txt models\lovdbyless_models

The output of such a command is given below.

unbounded_verif_sample_output

Optionally, we can add the -j option to perform property-based data model projection (described in our [ASE'12] paper) to simplify the formula before sending it to the solver. This may be helpful if the solver times out during the verification, which can happen due to the complexity of the verification queries.

Example #3

Finally, to use iDaVer to do automated property inference, the only command-line arguments provided is the name of the directory containing the model files of the application:

>ruby iDaVer.rb models\lovdbyless_models

iDaVer automatically infers properties using the heuristics described in our [ISSTA'13] paper. Next, iDaVer automatically checks whether the properties hold using unbounded verification. The results are output in CSV format:

Property	Solver	Num_ vars	Num_ clauses	Verif_ time	Verif_ result	Repair
transitive2[Profile, ForumTopic, ForumPost]	z3	92	131	0.025	fail	Add the ':through => :forum_topics' option to the association in the Profile class. Remove the 'belongs_to :profile' in the ForumPost class as well.
deletePropagation[Profile, Feed]	z3	139	297	0.130	fail	Add the ':dependent => :destroy' option to the association in the Profile class.
deletePropagation[ForumTopic, ForumPost]	z3	139	298	0.047	pass
deletePropagation[Profile, Photo]	z3	139	299	0.039	fail	Add the ':dependent => :destroy' option to the association in the Profile class.
...	...	...	...	...	...	...

Publications

[ISSTA’13] Jaideep Nijjar and Tevfik Bultan. "Data Model Property Inference and Repair." Proceedings of the 2013 International Symposium in Software Testing and Analysis (ISSTA 2013), Lugano, Switzerland, July 15-20, 2013.

[FormaliSE’13] Jaideep Nijjar, Ivan Bocic and Tevfik Bultan. "An Integrated Data Model Verifier with Property Templates." Proceedings of the ICSE 2013 Workshop on Formal Methods in Software Engineering (FormaliSE 2013), pages 29-25, San Francisco, USA, May 25, 2013.

[ASE’12] Jaideep Nijjar and Tevfik Bultan. "Unbounded Data Model Verification Using SMT Solvers." Proceedings of the 27th IEEE/ACM International Conference on Automated Software Engineering (ASE 2012), pages 210-219, Essen, Germany, September 3-7, 2012.

[ISSTA’11] Jaideep Nijjar and Tevfik Bultan. "Bounded Verification of Ruby on Rails Data Models." Proceedings of the 2011 International Symposium on Software Testing and Analysis (ISSTA 2011), pages 67-77, Toronto, Ontario, Canada, July 17-21, 2011.