基于Petri网的状态机变迁的形式化方法研究

摘要：

UML状态机图用来描述一个特定对象生命周期经历各种状态,尽管其表达简单明了,易于理解,但它缺乏准确语义,难以对其进行语义分析和验证的问题。变迁作为状态机图的重要组成部分,同样存在这样的问题，而Petri网有严格的形式化语义,而且有许多成熟的分析方法。为了分析状态机变迁,提出了TES模型,它可以描述状态机的触发器事件和监护条件等元素,然后将几种复合变迁用Petri网描述,最后给出了一个实例,说明模型之间是语义等价的。

关键词： Petri网 UML状态机图 触发器事件 监护条件 形式化方法 TES模型

作者: 何建伟 姚淑珍

作者单位: 北京航空航天大学计算机学院 北京 100083

会议类型: 国内会议

会议名称: 第十一届全国Petri网理论与应用学术年会

会议地点: 大连

会议语种:中文

页码: 65-68

在线出版日期: 2007-08-01（万方平台首次上网日期，不代表论文的发表时间）