Translating UML State Machines to Coloured Petri Nets Using Acceleo: A Report

Étienne André
(Université Paris 13, Sorbonne Paris Cité, LIPN, CNRS, UMR 7030, F-93430, Villetaneuse, France)
Mohamed Mahdi Benmoussa
(Université Paris 13, Sorbonne Paris Cité, LIPN, CNRS, UMR 7030, F-93430, Villetaneuse, France)
Christine Choppy
(Université Paris 13, Sorbonne Paris Cité, LIPN, CNRS, UMR 7030, F-93430, Villetaneuse, France)

UML state machines are widely used to specify dynamic systems behaviours. However its semantics is described informally, thus preventing the application of model checking techniques that could guarantee the system safety. In a former work, we proposed a formalisation of non-concurrent UML state machines using coloured Petri nets, so as to allow for formal verification. In this paper, we report our experience to implement this translation in an automated manner using the model-to-text transformation tool Acceleo. Whereas Acceleo provides interesting features that facilitated our translation process, it also suffers from limitations uneasy to overcome.

In Jun Pang and Yang Liu: Proceedings Third International Workshop on Engineering Safety and Security Systems (ESSS 2014), Singapore, Singapore, 13 May 2014, Electronic Proceedings in Theoretical Computer Science 150, pp. 1–7.
Published: 3rd May 2014.

ArXived at: http://dx.doi.org/10.4204/EPTCS.150.1 bibtex PDF
References in reconstructed bibtex, XML and HTML format (approximated).
Comments and questions to: eptcs@eptcs.org
For website issues: webmaster@eptcs.org