SyVOLT

This is the repository for the SyVOLT contract verification tool.

Objective

We address the issue of model transformation verification with our technique for verifying visual pre-/post-condition contracts on DSLTrans model transformations. A contract is said to hold on a transformation if it holds on the transformation’s input- output pairs. That is, for all input models where the contract’s pre-condition holds, the contract’s post-condition also holds in the corresponding output model produced by executing the transformation. Traceability constraints between the elements of the input and output models may also be required. Otherwise, the contract does not hold, and consequently, the transformation does not correctly implement the contract.

For more information, including a demo of the prover: SyVOLT Contract Prover Video

Installation

Please see the INSTALL.txt file in this directory.

The main development and usage platform is Linux. SyVOLT may not work on MacOS or Windows.

Usage

Command-line

• Run the test script using Python
  • Example: 'python test_atlTrans_extended.py'
• Use the argument --help to see some useful arguments
  • --slice=N will slice the transformation for contract N
  • --contract=N will select only one contract to prove, but will not slice
  • --verbosity=2 will output many details of path condition construction
  • --load will attempt to load PCs generated previously, to begin contract proving immediately

Eclipse

• Install the DSLTrans and SyVOLT plugins to edit and visualize the transformations and contracts
• Run the ANT script (such as verify_mbeddr.xml) to start the prover

MPS

The MPS plugin can be downloaded at: https://plugins.jetbrains.com/plugin/10385-dsltrans Please see the plugin repository for usage instructions: https://github.com/mbeddr/language_verification/blob/master/README.md

Mutation Testing

The script for each transformation can take parameters to mutate individual rules.

For example, here is one mutation of the Families-To-Persons transformation: python3 test_atlTrans_extended.py --rule_to_mutate=HCountry2Community --mutate=('ADD_CLASS','Family',True,0) --unit_contracts

• The actual mutation is performed in mutation/mutate.py

To perform wide-scale mutation testing, the main file is do_mutation_testing.py.

• This uses mutation/mutation_possibilities.py to generate all the mutations for each transformation
• Then the main transformation script is run for each possibility, with the appropriate mutation parameters

For example, run python3 do_mutation_testing.py F2P False to test all mutants for the Families-To-Persons transformation with the unit contracts. Change the False to True for the integration contracts.

The other transformations are: RSS, UML2ER, GM, Kiltera.

The mutation results will be collected in mutation_testing.xml. This is then the input into the Spectrum-Based Fault Localization Java program.

Related Work

[8] A Symbolic Execution-Based Approach To Model Transformation Verification using Structural Contracts. B. Oakes. Ph.D. dissertation, McGill University, 2018.

[7] Debugging of Model Transformations and Contracts in SyVOLT. B. Oakes, L. Lúcio, C. Verbrugge, H. Vangheluwe. Proceedings of MDEbug co-located with MODELS 2018, 532-537. 2018.

[6] Full Contract Verification for ATL using Symbolic Execution. B. Oakes, J. Troya, L. Lúcio, M. Wimmer. Software and Systems Modeling 2016 (pp. 1-35). Springer Berlin Heidelberg.

[5] SyVOLT: Full Model Transformation Verification Using Contracts. L. Lúcio, B. Oakes, C. Gomes, G. Selim, J. Dingel, J. R. Cordy, H. Vangheluwe. Proceedings of MODELS 2015.

[4] Finding and Fixing Bugs in Model Transformations with Formal Verification: An Experience Report. G. Selim, J. R. Cordy, J. Dingel, L. Lúcio, B. Oakes. Proceedings of Analysis of Model Transformations 2015 (pp. 26-35).

[3] Fully Verifying Transformation Contracts for Declarative ATL. B. Oakes, J. Troya, L. Lúcio, M. Wimmer. Proceedings of MODELS 2015 (pp. 256-265).

[2] A Technique for Symbolically Verifying Properties of Graph-based Model Transformations. L. Lúcio, B. Oakes, H. Vangheluwe. Technical Report SOCS-TR-2014.1, McGill University.

[1] Specification and Verification of Graph-Based Model Transformation Properties. G. Selim, L. Lúcio, J. Cordy, J. Dingel, B.Oakes. Proceedings of Graph Transformation 2014 (pp. 113-129). Springer International Publishing.