Simplified State Machine Execution Verification

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

Simplified State Machine Metamodel

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

• A State that is named and is contained in a CompositeState.
• Two kinds of pseudo states can be defined: InitialState and HistoryState each referencing a state of the composite state to which they belong. Each composite state must have one and only one initial state. Having an history state (but only one) is optionnal.
• The Transition element allows the definition of a transition betwen a source and a target states, associated with an Event that is simply defined with a name.
• A StateMachine is a special kind of composite state. It owns all transitions and events of the model and must be unique within the model.

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

• The isActive boolean attribute of State. It enables to set that a state is currently active or not.
• The referenced state of HistoryState that references the last active state of the composite state to which it belongs.

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.

Contracts

Three contracts have been implemented through ATL transformations:

• StateMachineInvariants.atl: It contains the OCL invariants associated with the meta-model and has to be applied with source models such as the step-X.xmi files.
• StateMachineStructuralUnmodification.atl: This is a unmodification contract ensuring that all structural elements (State, Transition ...) of the model have not been modified. It must then be applied on a source model containing concatenated models, such as the ones generated during the model execution. Notice that all mapping functions of this contract have been automatically generated with our mapping function generation tool.
• StateMachineRunToCompletion.atl: This is an execution contract ensuring that, depending on the associated event and active states, the right transition of the model has been triggered. This contract has to be applied on a source model containing concatenated models generated during the model execution.

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.