Simplified State Machine Execution Adaptation Verification

The Eclipse project StateMachineAdapt contained in adaptationContract.zip is implementing our simplified state machine execution engine and adaptation contracts. Put the uncompressed directory StateMachineAdapt in an Eclipse workspace and just import it.

Simplified State Machine Metamodel

StateMachine meta-model

Base of the meta-model

The base of the meta-model, defining an executable state machine, is the blue part.

The static part of the meta-model is composed of the following elements:

The dynamic part of the meta-model is simply composed of two elements:

Well-formedness rules

The well-formedness rules of the meta-model are directly embedded within the Ecore meta-model. Here are their description:

TODO

Extension for management of kinds of elements

All elements of the meta-model have been made specializing the Kind element for expressing "kinds" of elements. This extension is the gold part of the figure. The elementKind string attribute allows the definition of the string value, presented using the the <<...>> notation, of the elements for our train model in its variant (c).

Extension for management of contracts

The pink part of the figure is an automatic added part composed of elements dedicated to manage the checking of contracts. This part has been automatically added thanks to our the mapping function generator tool.

Files and model examples

The three versions of the train state machine presented in the paper are proposed in the project archive. Here are in details the files related to the meta-models and models:

Please not that all models (XMI files) are conforming to the StateMachineContract.ecore meta-model and not to StateMachine.ecore meta-model. From a pratical point of view, this has no impact concerning the contents of the models (no contract management elements are present in them) but this will make these models directly ready for contract checking.

To create a new state machine model, just use the EMF dynamic instantiation on the StateMachine element of the StateMachineContract.ecore meta-model. Then, build your model starting from this state machine root. For setting an initial state or an history state, there are 3 steps: 1) within a composite state, create an initial or history state child, 2) modify the initialState or historyState references of the composite state to reference these created states and 3) set referencedState for the initial state.

Execution engine

An execution engine for our simplified state machines has been implemented in Kermeta. It is the StateMachineExec.kmt program of the execution-engine folder.

The execution mainly consists in asking the user to enter the name of the next event to handle. If a corresponding transition exists for current active states, then this transition is triggered and active states of the state machine are modified.

For each step, that is for each event name entered by the user, the model in its current state is stored in a file named step-X.xmi in the exec-traces folder, where X is the number of the step. If required by the user, it generates also concatenated models (named step-concat-[X]-[X+1].xmi): for each event name, it concatenates the model before and the model after the event processing by the execution engine and adds the event name as the parameter of the contract operation in the concatenated model.

To help in using the engine, here is an example of the interaction with the user for executing the TrainB.xmi model:

  1. Directory of the model? [default=models] Just type "Return" to load a model from the "models" default folder.
  2. Name of the model file? Enter "TrainB.xmi"
  3. The contents of the model is then printed on the console, once the initial states of the state machine have been activated (an active state is marked with the (active) string following its name).
  4. Please choose the level of verification for event processing. 'exact', 'weak' or 'none' [default] : Enter the required value depending on what you want to do:
  5. Enter an event name ('end' to exit): enter the name of the next event to proceed (for instance "Amber", "Green", ...). Enter "end" to finish the execution.
  6. Enter 'Y' for generating the concatenated models (this can take a long time) or any key to quit the execution engine: enter "y" or "Y" to process the concatenation of the models generated during the execution, as explained above. This generation takes really a long time (due to Kermeta / EMF issues, or a programming problem ;-)

Note: do not forget to launch the Kermeta engine execution in a "Constrained Application" mode if you want to check event validity at runtime. If the program is runned in a normal mode, the precondition realizing the checking will not be evaluated.

Contracts

In addition to the event validity checking at runtime in the Kermeta engine, three static contracts have been implemented in OCL through an ATL transformations.

These contracts have been partially generated thanks to our mapping function generator (in a version under development, not the one of the project). For a given meta-model, the tool creates an ATL transformation fully duplicating a model with the addition of error elements in case of the non respect of OCL invariants. This is the base of the implementation of a contract: the designer has to modify the default generated empty invariants.

StaticEventChecking.atl

The static checking consists here in ensuring that for each excepted event, there exists a transition starting from each event (directly or from one of its super-states).

The set of expected events (colors for signals here) is directly expressed in the transformation, at line 26:

helper def: signalColors : Set(String) = Set{'Red', 'Amber', 'Green', 'Purple', 'White'};

The parameters of the transformation are the following:

Once the transformation executed, one has to look at the content of the generated file. If it contains only the initial state machine, it means that everything is ok. If it contains some ContractError instances in addition of the initial state machine, it means that some states do not process all events.

With the proposed parameters, there will be an error for each state of the state machine as the "White" color event is managed by none of the states for the (b) train state machine version. If removing this color from the set, the contract will be evaluated correctly.

StaticEventKindAndStateKindChecking.atl

The static checking consists here in ensuring that for each excepted event, there exists a transition starting from each event, based on its name or on its kind, and that this transition is leading to a state that has the same kind as the event.

Compared to the previous transformation, the set of events and their kinds is not embedded in the transformation but in an external file.

The parameters of the transformation are the following:

UnmodificationContract.atl

The goal of this contract is to ensure that a model is structurally equivalent to a reference model.

This contract is based on the unmodification contract principles: it checks after a tranformation that a source model is similar in its structure (hierarchy of states, transitions and events) than a target model. Here, there is no transformation carried out, but checking that a given model is similar to a reference model can be verified in the same way: this given model can play the role of the source model and the reference model the target one.

To check this kind of contract, the first step is to concatenate the source and the target model within a single third model. This action is realized through the "merge" feature or our mapping function generator tool, available through the MappingFunction.jar file of the mappingFunctionGenerator folder.

The parameters of the transformation are the following:

With the concatenated example, there is of course no error as the source and the target models are the same. Just modify some elements of the concatenated models to observe the generation of error elements in the evaluation model.