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 ws-executionContract.zip
is an Eclipse/EMF workspace containing two projects:
- UMLStateMachineContract : The UML state
machine execution presented in the paper:
- The definition of a UML
meta-model extension for specifying state machine instances
(structural extension and OCL invariants).
- The OCL contract
associated with the run_to_completion operation with model
examples.
- The MOCAS
platform is used for executing UML state machines and generate
models. However, notice that the current downloadable version does not
yet include the management of state machine instances (our UML
meta-model extension). We have to finalize its integration for an easy
and everybody use of the extended MOCAS version.
- 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.