Creating (correct) models isn’t an easy task. Modeling isn’t easy, and as it happens with any difficult task, the difficulty increases the chances of making mistakes. Developing software following MDE-based approaches is especially sensitive to the presence of errors in models since errors in the models get propagated to the final software.

The challenge of verifying model correctness is usually addressed by means of rigorous verification techniques based on the utilization of formal methods. The problem here,  though, is that modeling languages expressiveness usually causes these approaches to run into decidability issues and some of the measures taken to overcome this (like requiring  user-assistance to complete the verification process or limiting model expressiveness) can either affect their usability, or limit the complexity of the models that can be verified.

In our opinion, a model verification approach must be decidable, automatic and not limited to a certain subset of model constructs in order to be successfully and widely adopted. A possible way to get this is to follow a bounded verification approach which works by limiting the search space when verifying whether a given model satisfies a particular correctness property. The search space is the set of model instances that are created and analyzed when looking for a proof (i.e. an example) of the model correctness.  Limiting the search space means imposing limits in the number of instances that can be created, as well as in the values the attributes of the model constructs can take. Bounded verification is not free of shortcomings: results are only conclusive when a valid instance satisfying the correctness of the model is found. When it is not, we cannot be conclusive,  either the valid instance is out of the search space considered or the model doesn’t verify that property.

EMFtoCSP follows a bounded verification strategy to provide a pragmatical approach to model verification.  EMFtoCSP is an Eclipse-integrated tool for the verification of EMF models and UML class diagrams. OCL is also supported, so both types of models can be complemented with generic OCL constraints too.

The tool works by transforming the question of whether a given input model satisfies a particular correctness property into a Constraint Satisfaction Problem which is then fed into the underlying CSP solver. If the CSP solver finds a solution then a valid instance of the model is provided as a proof.

EMFtoCSP supports the following correctness properties:

• Strong satisfiability: A model is strong satisfiable when it’s possible to create a finite, non-empty instance in which all classes and associations are instantiated at least once.
• Weak satisfiability:  A model is weak satisfiable when it’s possible to create a finite, non-empty instance in which at least one class or one association is instantiated at least once.
• Lack of constraints redundancies: Two integrity constraints aren’t redundant when it’s possible to find a finite model instance in which only one of the two constraints are satisfied.
• Lack of constraints subsumptions:  Given two integrity constraints C1 and C2, C1 doesn’t subsume C2  when it’s possible to find a finite model instance in which C1 is satisfied and C2 is not.

Check this video to see the tool in action

For more details on the specifics of EMFtoCSP, you can read the paper we presented at the FormSERA workshop.

EMFtoCSP can be downloaded from the Eclipse labs project repository, here.

And if you’re still “shopping around” for a tool to help you evaluate the quality of your models, consider giving EMFtoCSP a try. We would even be more than happy to add other formalisms to the tool (so that the tool evolves to be not just EMFtoCSP but a family of EMFtoFM subcomponents, including EMFtoCSP but also EMFtoSMT and other translations). Everything can be discussed if there is a real interest. I’d really like you to avoid the not invented here syndrome ???? .

Remember also that there are many ways to contribute to an open source project so just helping to promote the tool, adding examples or extending the documentation would be invaluable.

 

Test Suite for EMFtoCSP

As a bonus, we’re glad to announce a new release of EMFtoCSP now including an auxiliary plugin to run regression and non-regression testing on EMFtoCSP and help ensure the quality of the code as we move forward with the tool development. EMFtoCSP is an Eclipse-integrated tool for the validation of EMF models and UML class diagrams. This post covers only the testing process. To know more about EMFtoCSP itself, we invite you to read the post about the tool.

While Regression testing ensures that recent code changes don’t have a negative impact on the already working functionalities, non-regression testing helps us determine if the changes we made have had the suitable effect. The following figure illustrates the process of the test suite plugin.

The test plugin relies on the JUnit framework. In particular, it uses the parameterized tests functionality which allows developers to run the same test using different values each time. The idea is to be able to automatically execute EMFtoCSP under different configurations thus skipping the need to use the current wizard for this.

In our case, each instance of a test is constructed using three arguments:

1. EMF/UML model.
2. A .properties file holding the configuration of the validation, i.e., properties to check (Strong/weak satisfiability, …), the population size, and a link to the OCL file if OCL constraints are not embedded directly in the model. Examples can be found here.
3. A boolean holding the predicted result: true if the solver should find a solution, false if not.

The test suite includes so far 20 cases with different properties. The cases vary from simple (testing specific model properties or OCL operations) to complex (either embedded or separated OCL invariants). To run the plugin : Right-click the tests project (i.e., fr.inria.atlanmod.emftocsp.tests) and select Run AS -> JUnit Plug-in Test. Below is the result you should get.

You can add your own test cases by putting your models and properties files (generated from the wizard) in the data folder and editing the method TestModelGeneration.data(). Please, feel free to contact for any further information (and if you do create your own tests, please consider also to submit them to the EMFtoCSP repository so that they become available also for other users).