run_to_completion operation specification

The project UMLStateMachineContract projet of the Eclipse workspace contained in ws-executionContract.zip is implementing the execution contract for the run_to_completion operation. It contains the following files:

• UMLwithActiveStateAndContractModified.ecore : The UML implementation in Ecore augmented with our extension for specifying state machine instances and managing contracts.
• Four complete execution steps corresponding to the execution of the run_to_completion operation for the microwave paper example. Each one contains, within a single concatenated model, the source and the target models of the step and the associated event:
  • Microwave-valid1.xmi : Active states are Closed::Baking for the source model and Open::Paused for the target one. The event is DoorOpen. The execution step is then valid (step 1 to step 2 of the paper example).
  • Microwave-valid2.xmi : Active states are Open::Paused for the source model and Closed::Baking for the target one. The event is DoorClosed. The execution step is then valid (step 2 to step 3 of the paper example, going back to the last state of Closed through the history state).
  • Microwave-invalid.xmi : Active states are Closed::Baking for the source model and Open::Paused for the target one. The event is Power. This execution step is not valid: on the target side, the Closed::Off state should have been active instead of Open::Paused.
  • Microwave-invalid-priority.xmi : Active states are Closed::Baking for the source model and Open::Off for the target one. The event is DoorOpen. This execution step is not valid: on the target side, the Open::Paused state should have been active. Indeed, the most internal transition associated with the DoorOpen event (from Baking to Paused) should have been triggered, regarding to the UML semantics. But here, the other transition leading to the initial state of Open (that is Off) has been triggered.
• Run_to_completion-Contract.atl : ATL transformation implementing the OCL invariant specifying the evolution contract of the run_to_completion operation. It checks if target active states are valid regarding to the source ones, the associated event and the transitions of the state machine.
• Contract-Result.xmi : Default file in which the contract evaluation result is stored. Concretely, it contains the associated execution step models and the evaluation result (Model -> Contract Base -> Contract Evaluation)

To check the validity of an execution step, one simply has to execute the ATL transformation. The source model is the file containing the execution step models, and the target model the file that will contain the contract evaluation result.

This workspace has been set up to work with Topcased V3.3 (ATL v3.0.1). Topcased is a software environment based on the Eclipse/EMF framework and dedicated to the realization of critical embedded systems.