Model checking manual

The core of a model checker is to verify constraints. A constraint is a condition or restriction expressed in natural language text or in a machine readable language for the purpose of declaring some of the semantics of an element.

To be able to build tool that use these constraints, they must be expressed using a machine readable language like OCL of Kermeta.

The language standardized by the OMG is OCL (Object Constraint Language). Kermeta can also natively express the same constraints. In order to use Kermeta runtime (interpreter or java compiler).

Since OCL behavior is a subset of Kermeta behavior, there is a transformation that allows to convert OCL constraint into kermeta ones, so the constraint can be used in any kermeta program (for example in a model checker, but also in other kind of application)

	Note
	In kermeta 1.3.2, we still need to manually do this conversion if we want to reuse OCL constraints in a kermeta program. However we plan to offer the possibility to directly include the OCL file in a kermeta program (ex: require "my.ocl") so the integration will be smoother.

By default, the structure of a metamodel will help a given editor to build a conformant model.

Typically, if you take uml metamodel, the tree editor is smart enough to not propose to add a Package into a Class, but will propose only concepts that can fit in it, for example an Operation.

Figure 1.1. Restriction of the proposal for model element creation driven by the metamodel structure

However, some constraints are difficult or impossible to capture using only the metamodel structure.

For example UML metamodel specification is complemented with a lot of constraints, typically expressed in OCL.

not self.allParents()->includes(self)

A typical translation of this contraint in kermeta will be : (TODO)

In order to implement a given process, it is sometime necessary to add some more constraints on a metamodel.

This will help to capture the intend behind the use of the given metamodel.

For example on a large metamodel like UML, we may want to use only a subset of it and even this subset can be used following some design rules. These addtional rules will help to specify the intend of the model, so it can be processed in a given way.

For example in a top down process, each step of the process may be expressed using UML, but at each step we add some more information and precision (typical MDA process) Even if each step use a valid UML model (regarding its structure and the standard constraints), a tool designed to work on a UML model of a given step might not work with an UML model of another process step.

In order to help the user detect the inconstancy, the basic idea is then to provide a set of invariant that are specific to a given step.

A model checker written in kermeta is dependent on its EMF (Eclipse Modeling Framework) implementation. It is designed to work with a specific metamodel.

If the model to check isn't in the correct format (for example in specific modeler format like Rhapsody) it is necessary to translate it (export) to the checker supported format.

Figure 2.1. Example : Export from Rhapsody modeler to the XMI format supported by EMF

Typically, the model checker can be integrated in the end user graphical interface. For example, in Mopcom project we have provided some popup actions for uml file resources, that allows to launch the various check on uml models.

Figure 2.2. Integration example of Mopcom model checkers using popup menu on uml files

	Tip
	You can find the procedure to provide such popup menu thet runs a kermeta program and the typical associated java code is presented in the logo tutorial (TODO add a link to the online version)

More advanced GUI integration are possible depending on the user integrated environment. For example, we may use the ability of eclipse to detect file changes to automatically run the check and report the failed invariant in the problem view. However, automatic check must be considered with care, since the user may need to have an incorrect model during some phase of his modeling process. A good practice would be to always propose to disable automatic check.

As the model checkers are sometime specific to a given development step in a process, we can also imagine to customize the user environment to propose and activate only the relevant checkers for the current process step.

Like any kermeta program, a model checker written in Kermeta can be run as a standalone application, for example on the command line. However, in this case, the main operation of the checker must ensure to report the failed invariants in a textual way.

For more information about running a kermeta application from the command line, please refer to the kermeta UI user guide http://www.kermeta.org/documents/ui_user_guide/

In Kermeta, you need to declare which metaclasses are known in your Kermeta program. This is acheived by using the require keyword which acts like an import. Then all class definition that are "required" will be available and known by your program. Otherwise you won't be able to load the model Ie. you can create an instance only of classes for which you know the definition !

3.1.1. General case

For checking your own metamodel, this is usually simple as you only need to add something like :

require "yourmetamodel.ecore"

You can directly require the ecore file because, if you need to have an extended version of a ClassDefinition, you can simply augment it using kermeta aspects.

Tip

If your ecore is deployed as a plugin you can also require the nsUri of the root package of your ecore inn ordr to get the version in EMF memory (in its registry). For ex: require "http://www.eclipse.org/emf/2002/Ecore" will get the version in memory, whereas require "platform:/plugin/org.eclipse.emf/ecore/model/Ecore.ecore" will get the file in the plugin org.eclipse.emf.ecore. Also note that these two require are incompatible in the same kermeta program since they connect to two similar but potentially different version of the same ClassDefinitions.

3.1.2. ClassDefintion of UML Profiles

In UML profiles, the stereotypes are a bit special because declaring a new stereotype definition is equivalent to declaring a new ClassDefinition that connects to the UML element (a uml::CLassifier, a uml::Package, a uml::LifeLine, etc).

The following figures show how a typical profiles is represented in a uml modeller (ie. what a uml end user see in his modeller) and what is actually in memory at the instance level (ie. at the metamodel level point of view, what is manipulated by a model transformation or model checker tool)

Figure 3.1. Stereotype declaration and instance as seen in a classical uml modeller

Figure 3.2. Stereotype use in a classical uml modeller

You can notice in (Figure 3.2, “Stereotype use in a classical uml modeller”) that the use of the stereotype is presented using some custom presentation, here it use the default presentation: name of the applied stereotype between double lower and greater, the stereotype atributes appears in a special tab in the property view.

Figure 3.3. Stereotype declaration and instance as seen from the metamodel point of view (ie. in an "ecore" modeller)

	Note
	This instance representation isn't specific to Kermeta, all modelling tools (including editors, model transformation tools, ...) use this representation internally even if they provide a simplified graphical representation.

You can notice several points :

• the stereotype object isn't contained by an uml element. Actually, they are stored at the root of the xmi file (usually side by sides with the root uml::Model element that contain the uml model)

• this link is navigable only in one direction, from the stereotype to the uml element.

Actually, the stereotype acts like a kind of decoration on top of the uml element, this was a requiremnt in uml specification in order to be able to load a uml model even if a specific tool don't know how to deal with a specific profile, the underlying uml model is still valid and can be processed.

This has some impacts on navigating in the model. For example, if from an uml element you want to know if it exists a stereotype that "decorate" the uml element, you'll have to navigate up to the resource ^[1] and then search within all the ob ject there if there is one that have a base_XXX property that points to the uml object ...

operation getClassifierStereotypes(aClassifier : uml::Classifier) : kermeta::standard::Sequence<kermeta::standard::Object> is do 
   var containingResource : kermeta::persistence::Resource init aClassifier.containingResource
   result := containingResource.select{ o |
      var base_ClassifierProperty : kermeta::language::structure::Property
      var classDefinition : kermeta::language::structure::ClassDefinition 
      classDefinition ?= o.getMetaClass.typeDefinition
      base_ClassifierProperty := classDefinition.allAttribute.detect { o | o.name.equals( "base_Classifier" ) } 		   
      o.get(base_ClassifierProperty) == aClassifier
   }		
end

	We have to look into the resource, in this case we guess (but we may be wrong!) that the stereotype is contained by the same resource (xmi file) as the uml element
	since we only know that the stereotype has a property named "base_Classifier" we have to use reflexivity
	If true then we have a stereotype of aClassifier

Example 3.1. Trivial but inefficient navigation in uml profiles

This is quite inefficient even on such simple request. A traditionnal approach would have been to use a cache (for exemple in a Hashtable), but even that isn't really satisfying. We will see in section Constraints on UML profiles how we can simplify the navigation using kermeta aspects.

The goal of this step is to get the model you want to check. It can be coupled to another process or model transformation written in Kermeta, however in most case, a simple resource load is usually enough to build a standalone checker.

var inputRepository : kermeta::persistence::EMFRepository init kermeta::persistence::EMFRepository.new 
var inputResource : kermeta::persistence::EMFResource
inputResource ?= inputRepository.createUMLResource(fileToLoad, "platform:/plugin/org.company.yourmetamodel/model/yourmetamodel.ecore")
inputResource.load()

inputResource.one 
inputResource.each{ rootElement | // do something on each element at the root of the Resource }
            

var inputRepository : kermeta::persistence::EMFRepository init kermeta::persistence::EMFRepository.new 
inputRepository.registerEcoreFile("platform:/plugin/org.eclipse.uml2.uml/model/UML.ecore") 
inputRepository.registerEcoreFile("platform:/plugin/org.eclipse.uml2.uml/model/UML_21.ecore")
inputRepository.ignoreLoadErrorUnknownProperty := true 
inputRepository.ignoreLoadErrorUnknownMetaclass := true
var inputResource : kermeta::persistence::EMFResource
inputResource ?= inputRepository.createUMLResource(fileToLoad, "platform:/plugin/org.eclipse.uml2.uml/model/UML.ecore")
inputResource.load()

This second step is the core part of the checker. It consist in writing the invariant constraints associated to the metaclasses of the model we want to check.

Actually, the context of the invariant (ie. the metaclass containing the invariant) constitute a kind of filter for the invariants. On a given element, only invariants that apply to this element will be checked. This also constitutes the basis for the organisation of the constraints because they will natively be displayed in their containing class.

For every combinaison of metamodel and intent, we need to write a set of constraints.

3.3.1. General case

As stated above, the invariant naturally applies to a metaclass. Kermeta aspect allows to reopen a metaclass definition, then adding an invariant to an existing metaclass is quite simple.

package uml;   // name of the package for these definition, the same as the one we want to aspectize


require kermeta
         // require the UML2 metamodel
require "http://www.eclipse.org/uml2/3.0.0/UML"

aspect class Classifier    // use aspect keyword in order to reopen the metaclass uml::Classifier
{
   inv inheritanceMustBeDirectedAndAcyclical is do
      not self.allParents().includes(self)  // the expression in the invariant must return false if the invariant is violated
   end
}

This sample adds an invariant to the metaclass uml::Classifier that checks that the inheritance is directed and doesn't have a cycle.

Example 3.4. Example of invariant definition on UML metamodel

Warning

Be careful, in this sample, the operation allParents is abstract in the metamodel. You must ensure to provide an implementation for it otherwise you'll get a NotImplementedException. In that sample, you can use the uml2 MDK and require the following file somewhere in your kermeta program: require "platform:/plugin/org.kermeta.uml2/src/kermeta/uml2_behavior.kmt" TODO : Implement this allParent() in uml MDK!!! A similar problem is when using derived properties for which you need to provide a behavior.

	Note
	Please note that the invariant name (inheritanceMustBeDirectedAndAcyclical in the above sample) may not be unique, however a good practice is to use a name as explicit as possible

Kermeta offers several operation that allows to

This chapter list some issues that my complexify the creation of a model checker. If possible, it also presents some cues towards resolving these problems.

	Note
	As this section presents some innovative ideas, if you have implemented some of them, please let us know and consider contributing your work to this document.