Formalizing UML State Machines for Automated Verification -- A Survey
Étienne André, Shuang Liu, Yang Liu, Christine Choppy, Jun Sun, Jin Song Dong
TL;DR
The paper analyzes two broad avenues for formalizing UML state machines to enable automatic verification: translation-based approaches that encode UML models into existing formal languages and direct operational-semantics approaches that specify inference rules over UML constructs. It surveys works from 1997 to 2021, comparing coverage of UML features, semantic foundations, and tool support across methods such as ASMs, EHAs, PROMELA, timed automata, Petri nets, CSP, PVS, B, Z, and institutional semantics. A key finding is that most translation-based methods cover only a subset of features and that many verification tools are no longer publicly available, raising concerns about reproducibility and long-term accessibility. In contrast, several direct semantic efforts (notably FS06/LLACSWD13) achieve broader feature coverage but often lack mature tooling. The study highlights the need for a more consistent, industry-oriented formalization with durable tool support and urges consideration of a minimal, extensible core UML subset to balance expressiveness with verifiability and practicality.
Abstract
The Unified Modeling Language (UML) is a standard for modeling dynamic systems. UML behavioral state machines are used for modeling the dynamic behavior of object-oriented designs. The UML specification, maintained by the Object Management Group (OMG), is documented in natural language (in contrast to formal language). The inherent ambiguity of natural languages may introduce inconsistencies in the resulting state machine model. Formalizing UML state machine specification aims at solving the ambiguity problem and at providing a uniform view to software designers and developers. Such a formalization also aims at providing a foundation for automatic verification of UML state machine models, which can help to find software design vulnerabilities at an early stage and reduce the development cost. We provide here a comprehensive survey of existing work from 1997 to 2021 related to formalizing UML state machine semantics for the purpose of conducting model checking at the design stage.