带有并发行为的UML状态机图的形式语义

Formal Semantics of UML State Machine Diagrams with Concurrent Behaviors

在软件开发过程中,UML(统一建模语言)状态机图是目前最流行的建模形式之一,它属于半形式化模型,无法用形式化的方法进行推理。为了能对UML状态机图进行推理,现有工作采用Petri网、时序逻辑语言XYZ/E、动态描述逻辑、Z(Object-Z)语言、CHAM化学抽象机等作为状态机图的形式语义,但这些语义都是行为语义,并没有从结构上直接形成体现真并发的形式语义。该文提出一种新的模型——统一结构模型作为带有并发行为的UML状态机图的形式语义,该模型不会增加或减少状态机图的任何信息。基于统一结构模型首先定义了状态机图的格局(全局状态),用于表现状态机图的执行过程,并且给出了UML状态机图的格局的转换规则,说明格局如何在状态机图中执行,在此基础上给出了状态机图的可达性算法,然后还对状态机图的死锁等性质进行了介绍,最后开发出一个原型工具,实现了状态机图的可达性分析,并用实例说明了该方法的应用。

In software development,UML(Unified Modelling Language)state machine diagrams are one of the most popular forms of modelling,which are semi-formal models and cannot be reasoned about in a formal way.In order to be able to reason about UML state machine diagrams,existing work uses Petri nets,temporal logic language XYZ/E,dynamic description logic,Z(Object-Z)language,CHAM chemical abstraction machine,etc.as the formal semantics of the state machine diagrams,but these semantics are behavioural semantics,and there is no formal semantics embodying the true concurrency directly from the structure.We propose a new model,the Unified Structural Model,as the formal semantics of UML state machine diagrams with concurrency behaviours,which does not add or subtract any information from the state machine diagrams.Based on the Unified Structural Model,firstly,the configuration(global state)of a state machine diagram is defined,which is used to represent the execution process of a state machine diagram,and the transformation rules of the configuration of a UML state machine diagram are given to illustrate how the configuration is executed in a state machine diagram,based on which the accessibility algorithms of state machine diagrams are given.Then properties such as deadlocks of state machine diagrams are also introduced.Finally,a prototype tool is developed that implements the accessibility analysis of state machine diagrams,and the application of the methodology is illustrated with examples.