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

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

Study on Formalization Method of State Machine Transition Based on Petri Net

UML state machine models the possible life histories of a specific object. Although it is expressive and understandable, it is hard to analyze and verify the state machine model because it lacks precise semantics. As an important component of state machine, transition has such problems too. However Petri net has a formal semantics and has many analysis methods available. To analyze the transition, a TES model is proposed here, which is able to describe trigger event and guard condition, Then several compound transitions are described with Petri net. Finally an example is given to explain the semantics between models is equivalent.