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

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