Translating UML State Machines to Coloured Petri Nets Using Acceleo: A Report
\'Etienne Andr\'e (Universit\'e Paris 13, France), Mohamed Mahdi, Benmoussa (Universit\'e Paris 13, France), Christine Choppy (Universit\'e, Paris 13, France)
TL;DR
This paper reports on automating the translation of UML state machines into Coloured Petri Nets using Acceleo, enabling formal verification of system behaviors, despite some limitations of the tool.
Contribution
It introduces an automated translation method from UML state machines to Coloured Petri Nets using Acceleo, facilitating formal verification.
Findings
Successful implementation of UML to Petri Nets translation
Identification of Acceleo's benefits and limitations for this task
Enhanced potential for formal verification of UML models
Abstract
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.
Peer Reviews
No public reviews on file for this paper yet. If you reviewed it on a platform where reviews are public (OpenReview, ICLR, NeurIPS, ICML), you can paste yours below so the community can read it here.
Videos
No videos yet. Explain this paper in a talk, walkthrough, or lecture? Add one.