  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.
