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.
Article PDF
Similar content being viewed by others
Explore related subjects
Discover the latest articles, news and stories from top researchers in related subjects.Avoid common mistakes on your manuscript.
References
Alur R, Yannakakis M (2001) Model checking of hierarchical state machines. ACM Trans Program Lang Syst 23(3): 273–303
Baier C, Katoen J-P (2008) Principles of model checking. The MIT Press, New York
Bergstra JA, Klop JW (1984) Process algebra for synchronous communicati. Inf Control 60(1–3): 109–137
Blom S, van de Pol J (2008) Symbolic reachability for process algebras with recursive data types. In: Proceedings on theoretical aspects of computing (ICTAC 2008). Lecture Notes in Computer Science, vol 5160. Springer, Berlin, pp 81–95
Blom SCC, van de Pol JC, Weber M (2009) Bridging the gap between enumerative and symbolic model checkers. Technical Report TR-CTIT-09-30, CTIT, University of Twente, Enschede
Cimatti A, Giunchiglia F, Mongardi G, Romano D, Torielli F, Traverso P (1998) Formal verification of a railway interlocking system using model checking. Formal Aspects Comput 10(4): 361–380
Damm W, Josko B, Pnueli A, Votintseva A (2005) A discrete-time UML semantics for concurrency and communication in safety-critical applications. Sci Comput Program 55: 81–155
Eriksson L-H (1996) Specifying railway interlocking requirements for practical use. In: Proceedings of the 15th international conference on computer safety, reliability and security (SAFECOMP’96). Springer, Berlin
Xie F, Levin V, Browne J (2001) Model checking for an executable subset of UML. In: 16th IEEE international conference on automated software engineering (ASE 2001), pp 333–336
Fokkink W (1996) Safety criteria for the vital processor interlocking at Hoorn-Kersenboogerd. In: 5th conference on computers in railways (COMPRAIL’96). Volume I: railway systems and management
Gnesi S, Latella D, Lenzini G, Abbaneo C, Amendola AM, Marmo P (2000) An automatic SPIN validation of a safety critical railway control system. In: Proceedings of the 2000 international conference on dependable systems and networks. IEEE Computer Society, Washington, DC, pp 119–124
Groote JF, Mathijssen A, Reniers MA, Usenko YS, van Weerdenburg M (2007) The formal specification language mCRL2. In: Proceedings of methods for modelling software systems, Dagstuhl seminar proceedings, vol 06351
Hu Z, Shatz SM (2006) Explicit modeling of semantics associated with composite states in UML statecharts. J Autom Softw Eng 13(4): 423–467
KnowGravity (2008) Cassandra/xUML user’s guide. http://www.knowgravity.com/eng/value/cassandra.htm
Mellor SJ, Balcer M (2002) Executable UML: a foundation for model-driven architecture. Addison Wesley, Reading
Object Management Group (2008) Semantics of a foundational subset for executable UML models. http://www.omg.org/spec/FUML/1.0/Beta1/PDF/. Accessed Nov 2008
Object Management Group (2009) OMG unified modeling language superstructure version 2.2. http://www.omg.org/spec/UML/2.2/Superstructure/PDF/. Accessed Feb 2009
Purandar B, Ramesh S (2004) Model checking of statechart models: survey and research directions. http://arxiv.org/abs/cs.SE/0407038. Accessed July 2004
Turner E, Treharne H, Schneider S, Evans N (2008) Automatic generation of CSP || B skeletons from xUML models. In: Proc. of Theoretical Aspects of Computing (ICTAC 2008), pp. 364–379
von der Beeck M (2001) Formalization of UML-statecharts. In: Proceedings UML 2001. Lecture Notes in Computer Science, vol 2185. Springer, Berlin, pp 406–421
Winter K, Robinson NJ (2003) Modelling large railway interlockings and model checking small ones. In: ACSC ’03: Proceedings of the 26th Australasian computer science conference, pp 309–316. Australian Computer Society, Inc.
Yeung WL, Leung KRPH, Wang J, Dong W (2005) Improvements towards formalizing UML state diagrams in CSP. In: Proceedings of the 12th Asia-Pacific software engineering conference (APSEC 2005). IEEE Computer Society
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.
Open Access
This article is distributed under the terms of the Creative Commons Attribution Noncommercial License which permits any noncommercial use, distribution, and reproduction in any medium, provided the original author(s) and source are credited.
Author information
Authors and Affiliations
Corresponding author
Rights and permissions
Open Access This is an open access article distributed under the terms of the Creative Commons Attribution Noncommercial License (https://creativecommons.org/licenses/by-nc/2.0), which permits any noncommercial use, distribution, and reproduction in any medium, provided the original author(s) and source are credited.
About this article
Cite this article
Hansen, H.H., Ketema, J., Luttik, B. et al. Towards model checking executable UML specifications in mCRL2. Innovations Syst Softw Eng 6, 83–90 (2010). https://doi.org/10.1007/s11334-009-0116-1
Received:
Accepted:
Published:
Issue Date:
DOI: https://doi.org/10.1007/s11334-009-0116-1