Simplified State Machine Execution Verification

The project StateMachine of the Eclipse workspace contained in is implementing simplified state machine execution and contracts.

Simplified State Machine Metamodel

StateMachine meta-model

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:

This meta-model is defined in the StateMachine.ecore file of the metaModels folder. The StateMachineContract.ecore file is the same meta-model augmented with the contract management elements as presented in the paper.

OCL invariants associated with the meta-models are defined in the StateMachineInvariants.atl ATL Transformation (see the contract section).

Model examples

The folder models contains the microwave state machine example of the paper. The Microwave.xmi and MicrowaveContract.xmi models are exactly the same with one exception: the first one is conformed to StateMachine.ecore and the second one to StateMachineContract.ecore (concretely, only the nsURI reference changes between the two files).

The MicrowaveRefined.xmi and MicrowaveRefinedContract.xmi models are the microwave refined version (the step 4 of the paper example): the Baking state is now a composite state (notice that compared to the paper example, an history state has been added in this composite state).

To create a new state machine model, just use the EMF dynamic instantiation on the StateMachine element of one of the Ecore meta-models. Then, build your model starting from this state machine root. Do not forget, for a composite state, to explicitely set references to its initial state and its potential history state. We suggest you to directly create a model conforming to the StateMachineContract.ecore, this will simplify contract verifications.

Model execution

An execution engine for our simplified state machine has been implemented in Kermeta. Two versions are available: StateMachineExec.kmt and StateMachineExecContract.kmt (in folder executionEngine). The first one works with a model conforming to StateMachine.ecore and the second one to StateMachineContract.ecore.

The execution 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 of the execTraces folder, where X is the number of the step. When using the StateMachineExecContract.kmt version, once the execution terminated, 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 treatment by the execution engine and adds the event name as the parameter of the contract operation in the concatenated model. This execution engine version is thus preferable to use as it directly generates required concatenated models for verifying execution contracts.

By default, the executed state machine is our microwave example. To execute another state machine, edit the Kermeta file and modify in the "main" operation (at the end of the file) the "platform:/resource/StateMachine/models/Microwave[Contract].xmi" string to reference your XMI file.


Three contracts have been implemented through ATL transformations:

Notice that all of these transformations are working with models conforming to StateMachineContract.ecore. As a consequence, for "SMCSource" and "SMCTarget" parameters of each transformation, you have to reference this meta-model. You can use the contractEvaluations folder for storing contract evaluation results. Each result file is a copy of the source file including in the ContractBase element a reference to a ContractEvaluation element allowing to know if the contract is respected or not through its globalResult attribute. If not, ContractError elements have also been created and added in the result model.

Mapping Function Generator

The project also contains the mapping function generator tool, through the MappingFunction.jar file of the folder MappingFunctionGenerator.