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

来源：计算机技术与发展杂志2024年第05期北京时间：

作者：陈华豪;蒋建民;谢嘉成;陈卓然;唐国富;

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

关键词：统一建模语言;状态机图;形式化模型;并发行为;可达性;死锁