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.

翻译：统一建模语言（UML）是动态系统建模的标准规范。UML行为状态机用于对面向对象设计的动态行为进行建模。由对象管理组织（OMG）维护的UML规范采用自然语言（而非形式化语言）进行描述。自然语言固有的模糊性可能导致最终状态机模型存在不一致性。形式化UML状态机规范旨在解决这种模糊性问题，并为软件设计者和开发者提供统一视图。此类形式化工作同时致力于为UML状态机模型的自动验证奠定基础，有助于在早期阶段发现软件设计缺陷并降低开发成本。本文系统综述了1997年至2021年间为在设计阶段进行模型检测而开展的UML状态机语义形式化相关研究工作。