iDaVer [an Integrated DAta model VERifier]
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.
RequirementsThe 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.
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.|
For the examples below, we will use LovdByLess, an open-source, social networking application.
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):
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:
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.
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.
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.
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[Profile, Photo]||z3||139||299||0.039||fail||Add the ':dependent => :destroy' option to the association in the Profile class.|
[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.