In the MACHINAIDE project we verify Cordis models by means of mCRL2. Cordis models are UML-like models developed, tested and simulated in the Cordis SUITE.
In this presentation I will take you along on our journey towards verification of Cordis models in three parts:
- Description of the structure and semantics of Cordis models
- Peculiarities in the implementation of these models (how did we discover them? how do we deal with them?)
- Discussion of the verification of an industrial model of a pneumatic cylinder.