基于Petri网的UML状态图的形式化模型

提出一种可以准确描述UML状态图动态特征的形式化模型SC_Net.首先给出了UML状态图的形式化语法定义,其中用状态集合、转移集合、事件集合、条件集合、活动集合、对象集合和变量集合,定义了一系列辅助函数描述UML状态图特征,用确定目标状态和受限源状态表示层次关系,用开放事件和封闭事件表示对象之间的消息.基于C_Net定义了描述UML状态图动态语义的Petri网模型SC_Net,既能描述状态图中的控制部分,又能描述状态图中的数据处理部分,并给出了从UML状态图到SC_Net的转换步骤,便于实现自动转换过程.最后以柔性制造系统的一个实例说明SC_Net能用于分析UML状态图的性质.

Formal models of UML statechart diagrams based on Petri nets

A formal model named SC_Net which can precisely describe the dynamic features of UML statechart diagrams was presented.Firstly a formal syntactic of UML statechart diagrams was given and a series of auxiliary functions to describe the structure features of UML statechart diagrams were presented in which target determinator and source restriction were used to describe the inter-level transitions and open events and close events were used to describe the communication among UML statechart diagrams.Then,based on C_Net an extended Petri net model named SC_Net was defined which can be used for the semantic models of UML statechart diagrams.Besides the control parts,SC_Net also included the data process parts which was lacked in the research area of formal semantics of UML statechart diagrams.The translation process from UML statechart diagrams to SC_Net was defined.At last,an example in flexible manufacture systems was given.Results show that SC_Net can be used to verify the properties of the UML statecharts.