Creating (correct) models isn’t  an easy task. Modeling isn’t easy, and as it happens with any difficult task, difficulty increases the chances of making mistakes. Developing software following MDE-based approaches is specially 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 expresiveness 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 expresiveness) 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 analysed 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 is satisfied.
• Lack of constraints subsumptions:  Given two integrity constraints C1 and C2, C1 doesn’t subsumes 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.