The technical results and ressources presented in the ECMFA'11 paper are available on this page.

OCL contract for the run_to_completion operation

If you simply want to have a quick look at the contract presented in the paper (the specification of the run_to_completion operation), just open the Run_to_Completion-Contract.atl file.

Tools and resources for verifying model execution through contracts

The archive is an Eclipse/EMF workspace containing two projects:

  1. UMLStateMachineContract : The UML state machine execution presented in the paper:
  2. StateMachine : As the UML state machine execution contract is somehow hard to apprehend because of the UML meta-model complexity, we have implemented a simplified state machine meta-model with its associated execution engine and contracts. The project also contains the mapping function generator tool allowing the automatic modification of meta-models, model concatenation and generation of mapping functions for writing contracts.