university website

H.H. Hansen (Helle), J. Ketema, S.P. Luttik (Bas), M.R. Mousavi and J.C. van de Pol (Jaco)

2010

Towards Model Checking Executable UML Specifications in mCRL2

Publication

Publication

Innovations in Systems and Software Engineering , Volume 6 p. 83- 90

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.
Additional Metadata
Keywords Software verification and validation, Specification languages, Model checking, Executable UML, Process algebra
MSC Specification and verification (program logics, model checking, etc.) (msc 68Q60), Models and methods for concurrent and distributed computing (process algebras, bisimulation, transition nets, etc.) (msc 68Q85)
THEME Software (theme 1)
Publisher Springer
Journal Innovations in Systems and Software Engineering
Organisation Computer Security
Citation
Hansen, H., Ketema, J., Luttik, B., Mousavi, M. R., & van de Pol, J. (2010). Towards Model Checking Executable UML Specifications in mCRL2. Innovations in Systems and Software Engineering, 6, 83–90.
Free Full Text ( Final Version )

Additional Files
Publisher Version


User Publication Person Organisation Collection
Close