北京航空航天大学学报 ›› 2007, Vol. 33 ›› Issue (02): 248-252.

• 论文 • 上一篇    

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

郭峰, 姚淑珍   

  1. 北京航空航天大学 计算机学院, 北京 100083
  • 收稿日期:2006-01-05 出版日期:2007-02-28 发布日期:2010-09-19
  • 作者简介:郭 峰(1972-),男,山东宁津人,博士生,guofeng_buaa@163.com.
  • 基金资助:

    航空科学基金资助项目(O1F51052)

Formal models of UML statechart diagrams based on Petri nets

Guo Feng, Yao Shuzhen   

  1. School of Computer Science and Technology, Beijing University of Aeronautics and Astronautics, Beijing 100083, China
  • Received:2006-01-05 Online:2007-02-28 Published:2010-09-19

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

Abstract: 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.

中图分类号: 


版权所有 © 《北京航空航天大学学报》编辑部
通讯地址:北京市海淀区学院路37号 北京航空航天大学学报编辑部 邮编:100191 E-mail:jbuaa@buaa.edu.cn
本系统由北京玛格泰克科技发展有限公司设计开发