UML状态机的形式语义

The Formal Semantics of UML State Machine

许多大型系统在进行分析和设计时,均采用UML作为需求描述语言,尤其是一些对安全性要求较高的系统,更是广泛采用UML的动态行为描述机制——状态机来描述协议及控制机制.但是,由于UML没有形式化的动态语义,不利于对其所描述的需求进行形式化验证和证明,为了解决这一问题,采用以下方法为UML状态机构建形式语义.把UML状态机中的状态映射到一种项代数上,用归纳的状态项表示状态机的状态.然后,把状态项映射到一种加标记的变迁系统LTS上,LTS-状态是状态机的状态项,LTS-变迁是UML状态机的微步.最后,用Plotkin风格的结构操作语义SOS(structural operational semantics)规则归纳地给出满足组合性的UML状态机语义.此方法既是对一些经典Statechart形式化方法的综合,又针对UML状态机的特点作了创新,使状态项能够动态地描述任意时刻UML状态机的配置树,简化LTS的标记,同时,结构化的语义规则更为形式化验证奠定了基础.

More and more large systems are taking UML as requirements description language for system analysis and design, especially in those safety-critical systems. One of the most important dynamic behaviorspecifying mechanism of UML---the UML state machine, is widely used for specification of communicationprotocols and control units. Unfortunately, UML has no strictly defined formal dynamic semantics. It is difficult to do formal verification and proof on the requirements. In this paper, a formal semantics of UML state machine is built. The UML state is firstly represented by inductive state term from some kind of term algebra. Secondly, a labeled transition system (LTS) is introduced, in which an LTS-state is a UML state term, an LTS-transition is a micro step of UML state machine. In the end, a set of Plotkin-style structural operational semantics (SOS) rules inductively defines a compositional formal semantics for UML state machine. This method not only synthesizes those formal methods for classical Statecharts, but also makes innovation addressed to UML state machine. At any time, the configuration of the machine can be inferred from the state term. The simplified LTS-Iabel and structuralized operational semantics rules will play a fundamental role in formal verification.