Translating UML State Machines to Coloured Petri Nets Using Acceleo: A Report
Software Engineering
2014-05-07 v1 Logic in Computer Science
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.
Keywords
Cite
@article{arxiv.1405.1112,
title = {Translating UML State Machines to Coloured Petri Nets Using Acceleo: A Report},
author = {Étienne André and Mohamed Mahdi Benmoussa and Christine Choppy},
journal= {arXiv preprint arXiv:1405.1112},
year = {2014}
}
Comments
In Proceedings ESSS 2014, arXiv:1405.0554