Publications:Towards model checking executable UML specifications in mCRL2

From CERES
Revision as of 05:43, 26 June 2014 by Slawek (Talk | contribs)

(diff) ← Older revision | Latest revision (diff) | Newer revision → (diff)
Jump to: navigation, search

Do not edit this section

Keep all hand-made modifications below

Title Towards model checking executable UML specifications in mCRL2
Author Helle Hvid Hansen and Jeroen Ketema and Bas Luttik and Mohammad Reza Mousavi and Jaco van de Pol
Year 2010
PublicationType Journal Paper
Journal Innovations in Systems and Software Engineering
HostPublication
DOI http://dx.doi.org/10.1007/s11334-009-0116-1
Conference
Diva url http://hh.diva-portal.org/smash/record.jsf?searchId=1&pid=diva2:584486
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.