Abstract
We describe a translation of a subset of executable UML (xUML) into the process algebraic specification language mCRL2. This subset includes class diagrams with class generalisations, and state machines with signal and change events. The choice of these xUML constructs is dictated by their use in the modelling of railway interlocking systems. The long-term goal is to verify safety properties of interlockings modelled in xUML using the mCRL2 and LTSmin toolsets. Initial verification of an interlocking toy example demonstrates that the safety properties of model instances depend crucially on the run-to-completion assumptions.
| Original language | English |
|---|---|
| Pages (from-to) | 83-90 |
| Number of pages | 8 |
| Journal | Innovations in Systems and Software Engineering |
| Volume | 6 |
| Issue number | 1-2 |
| DOIs | |
| Publication status | Published - 1 Mar 2010 |
Funding
Acknowledgments This research is partially funded by the European Comission (EC), as a grant to the FP7 project INESS, grant agreement no. 218575. Any opinions, findings and conclusions or recommendations expressed in this material are those of the authors and do not necessarily reflect the views of either the EC or the INESS consortium.
Keywords
- Executable UML
- Model checking
- Process algebra
- Software verification and validation
- Specification languages
Fingerprint
Dive into the research topics of 'Towards model checking executable UML specifications in mCRL2'. Together they form a unique fingerprint.Cite this
- APA
- Author
- BIBTEX
- Harvard
- Standard
- RIS
- Vancouver