Towards Model Checking Executable UML Specifications in mCRL2

Hansen, Helle Hvid and Ketema, Jeroen and Luttik, Bas and Mousavi, MohammadReza and Pol van de, Jaco (2010) Towards Model Checking Executable UML Specifications in mCRL2. Innovations in Systems and Software Engineering, 6 (1-2). pp. 83-90. ISSN 1614-5046

Preview

PDF
315Kb

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.
Item Type:	Article
Copyright:	© 2010 The Author(s)
Faculty:	Electrical Engineering, Mathematics and Computer Science (EEMCS)
Research Group:	Formal Methods and Tools (FMT)
Link to this item:	http://purl.utwente.nl/publications/70349
Official URL:	http://dx.doi.org/10.1007/s11334-009-0116-1
Export this item as:	BibTeX EndNote HTML Citation Reference Manager

Show download statistics for this publication

Repository Staff Only: item control page

Metis ID: 277400