Helle Hvid Hansen, Jeroen Ketema, Bas Luttik, MohammadReza Mousavi and Jaco van de Pol. Proceedings of the 2nd IEEE International workshop UML and Formal Methods ( UML&FM 2009), Rio de Janeiro, Brazil, December 2009.
We describe a formalisation of a subset of Executable UML (xUML) in the process algebraic specification language \mcrl2. This formalisation includes class diagrams with class generalisations and state machines with send 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 has demonstrated that the safety properties of model instances depend crucially on the run-to-completion assumptions made.
Paper in .pdf format in .ps format
Bibtex Entry:
@inProceedings{INESSD4-09,
author = "Hansen, Helle Hvid and Ketema, Jeroen and Luttik, Bas and Mousavi, MohammadReza and van de Pol, Jaco",
title = "Towards Model Checking Executable UML Specifications in mCRL2",
booktitle = "Proceedings of the 2nd IEEE International workshop UML and Formal Methods ({UML\&FM 2009})",
year = "2009"
}