A Formal Semantics for the Complete Syntax of UML State Machines with Communications (Report)
Shuang Liu, Yang Liu, Etienne Andr, Christine Choppy, Jun Sun, Bimlesh Wadhwa, Jin Song Dong · 2013
UML is a widely used notation introduced by the Object Management Group (OMG), and formalizing its semantics is an important issue. In this work, we concentrate on formalizing UML state machines which are used to express the dynamic behavior of software systems. We propose a formal operational semantics covering all features of the latest version (2.4.1) of UML state machine specification. We use Labeled Transition System (LTS) as the semantic model of UML state machines, which is subject to automatic verification techniques like model checking. Furthermore, our proposed semantics includes synchronous and asynchronous communications between state machines. We implement our approach in USMC, a model checker supporting editing, simulation and automatic verification of UML state machines. Experiments show the effectiveness of our approach.