Formal modeling and analysis of UML statecharts
-
摘要: 为解决状态图的建模问题,特别是带有复合状态的层次化状态图的建模问题,分析了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.
-
Key words:
- model buildings /
- Petri nets /
- semantics /
- analysis
-
[1] Bouabana T T, Belmesk M. Formalization of UML object dynamics and behavior 2004 IEEE International Conference on Systems, Man and Cybernetics. Hague:IEEE,2004:4971-4976 [2] Saldhana J A, Shatz S M. UML diagrams to object Petri net models:an approach for modeling and analysis Proceedings of the Int Conference on Software Engineering and Knowledge Engineering (SEKE). Chicago:Knowledge Systems Insitute, 2000:103-110 [3] Hu Z, Shatz S M. Explicit modeling of semantics associated with composite states in UML statecharts[J]. Journal of Automated Software Engineering, 2006, 13(4):423-467 [4] 钱俊彦,蔡国永,古天龙,等. Startchart规格语言的语法分析研究[J]. 林电子工业学院学报,1999, 19(3):40-44 Qian Junyan,Cai Guoyong, Gu Tianlong, et al. Research on syntax analysis of statechart specification[J]. Journal of Guilin Institute of Electronic Technology, 1999,19(3):40-44 (in Chinese) [5] Heimdahl M P, Leveson N G. Completeness and consistency checking of state-Based software requirements[J]. IEEE Transaction on Software Engineering, 1996,22(6):363-377 [6] Murata T. Petri nets:properties, analysis and applications[J].Proceedings of the IEEE, 1989,77(4) :541-580
点击查看大图
计量
- 文章访问数: 2864
- HTML全文浏览量: 122
- PDF下载量: 1231
- 被引次数: 0