Publication Type
Conference Proceeding Article
Version
publishedVersion
Publication Date
6-2013
Abstract
UML is a widely used notation, and formalizing its semantics is an important issue. Here, we concentrate on formalizing UML state machines, used to express the dynamic behaviour of software systems. We propose a formal operational semantics covering all features of the latest version (2.4.1) of UML state machines specification. We use labelled transition systems as the semantic model, so as to use automatic verification techniques like model checking. Furthermore, our proposed semantics includes synchronous and asynchronous communications between state machines. We implement our approach in USM2C, a model checker supporting editing, simulation and automatic verification of UML state machines. Experiments show the effectiveness of our approach.
Keywords
State Machine, Model Check, Formal Semantic, Linear Temporal Logic, Event Pool
Discipline
Software Engineering
Research Areas
Software and Cyber-Physical Systems
Publication
Proceedings of the 10th International Conference, IFM 2013 Turku, Finland, June 10-14
First Page
331
Last Page
346
ISBN
9783642386121
Identifier
10.1007/978-3-642-38613-8_23
Publisher
Springer Link
City or Country
Turku, Finland
Citation
LIU, Shuang; LIU, Yang; ANDRÉ, Étienne; CHOPPY, Christine; SUN, Jun; WADHWA, Bimlesh; and DONG, Jin Song.
A formal semantics for complete UML state machines with communications. (2013). Proceedings of the 10th International Conference, IFM 2013 Turku, Finland, June 10-14. 331-346.
Available at: https://ink.library.smu.edu.sg/sis_research/5003
Creative Commons License
This work is licensed under a Creative Commons Attribution-NonCommercial-No Derivative Works 4.0 International License.
Additional URL
https://doi.org/10.1007/978-3-642-38613-8_23