北京航空航天大学学报 ›› 2007, Vol. 33 ›› Issue (04): 472-476.

• 论文 • 上一篇    下一篇

UML状态图的形式化建模及其分析

姚淑珍, 金茂忠   

  1. 北京航空航天大学 计算机学院, 北京 100083
  • 收稿日期:2006-12-15 出版日期:2007-04-30 发布日期:2010-09-19
  • 作者简介:姚淑珍(1965-),女,黑龙江佳木斯人,教授,szyao@buaa.edu.cn.

Formal modeling and analysis of UML statecharts

Yao Shuzhen, Jing Maozhong   

  1. School of Computer Science and Technology, Beijing University of Aeronautics and Astronautics, Beijing 100083, China
  • Received:2006-12-15 Online:2007-04-30 Published:2010-09-19

摘要: 为解决状态图的建模问题,特别是带有复合状态的层次化状态图的建模问题,分析了UML状态图的结构特点和语义特征,构造了层次化着色Petri网HCPN.将复合状态的Petri网子网结构划分成输入/输出端口、状态迁移部分和历史状态部分.其中输入/输出端口分别用于完成子网进入弧的解析和离开的弧的汇总,状态迁移部分完成状态机子网内部状态变换,历史状态部分通过"记忆单元",完成复合状态的"记忆恢复"和"记忆刷新".基于所构造的HCPN结构,总结了状态图复合状态转入/转出迁移的语义和约束规则,阐述了复合状态的Petri网子网的相应描述方法和分析技术.最后针对状态图的安全性要求详细论述了历史状态完备性判定原则、父子层一致性判定原则和状态可达性判定原则的HCPN语义表示.研究成果对进一步开发自动化分析验证工具,优化复杂系统设计方案,提高软件质量具有重要的指导意义.

Abstract: The structural and semantic features of UML statecharts are analyzed firstly, and the hierarchical colored Petri net(HCPN) is constructed to solve modeling issues,especially those related to hierarchical statecharts with composite states. The Petri subnet for a composite state is composed of input/output interfaces, a state-transition part and a history state part. The input/output interfaces are used to parse entry arcs and gather exiting arcs to/from composites respectively. The state-transition part realizes transitions of the internal states. The history state part deals with memory recovery and memory cleanup of history units. After abstracting semantic rules and constrains of entry/exit transitions, their descriptions and analysis techniques of composite states based on HCPNs are illustrated. Finally, in the view of safety of UML statechart, HCPN semantic representation for completeness, consistency and reachability of statechart is elaborated. Optimizing the design of complex systems the guide in theory and practice for further research on developing automatic verification tools is provided.

中图分类号: 


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