A Proven Translation from a UML State Machine Subset to Timed Automata

Abstract

Although Unified Modeling Language (UML) state machines constitute a convenient modeling formalism that is widely used in many applications, the lack of formal semantics impedes carrying out automatic processing, such as formal verification. In this article, we aim to achieve a proven translation from a subset of UML state machines to timed automata. A generic abstract syntax is defined for state machines that allows us to specify state machines as a tree-like structure, explicitly illustrating the hierarchical relationships within the model. Based on this syntax, a formal asynchronous semantics for state machines and systems of state machines is established. Additionally, the semantics of timed automata is specified. Then, a translation relation from the considered set of state machines to timed automata is defined and a strong equivalence relation - namely, a timed bisimulation between the source and target models - is formally proven. The proof is carried out inductively while considering continuous (time) and discrete transitions separately. This proof allows us to demonstrate a strong similitude between these models.