| UML状态图的形式化建模及其分析 |
| |
| 引用本文： | 姚淑珍,金茂忠.UML状态图的形式化建模及其分析[J].北京航空航天大学学报,2007,33(4):472-476. |
| |
| 作者姓名： | 姚淑珍 金茂忠 |
| |
| 作者单位： | 北京航空航天大学,计算机学院,北京,100083;北京航空航天大学,计算机学院,北京,100083 |
| |
| 摘 要： | 为解决状态图的建模问题,特别是带有复合状态的层次化状态图的建模问题,分析了UML状态图的结构特点和语义特征,构造了层次化着色Petri网HCPN.将复合状态的Petri网子网结构划分成输入/输出端口、状态迁移部分和历史状态部分.其中输入/输出端口分别用于完成子网进入弧的解析和离开的弧的汇总,状态迁移部分完成状态机子网内部状态变换,历史状态部分通过"记忆单元",完成复合状态的"记忆恢复"和"记忆刷新".基于所构造的HCPN结构,总结了状态图复合状态转入/转出迁移的语义和约束规则,阐述了复合状态的Petri网子网的相应描述方法和分析技术.最后针对状态图的安全性要求详细论述了历史状态完备性判定原则、父子层一致性判定原则和状态可达性判定原则的HCPN语义表示.研究成果对进一步开发自动化分析验证工具,优化复杂系统设计方案,提高软件质量具有重要的指导意义.
|
| 关 键 词： | 建模 Petri网 语义 分析 |
| 文章编号： | 1001-5965(2007)04-0472-05 |
| 收稿时间： | 2006-12-15 |
| 修稿时间： | 2006-12-15 |
Formal modeling and analysis of UML statecharts |
| |
| Yao Shuzhen,Jing Maozhong.Formal modeling and analysis of UML statecharts[J].Journal of Beijing University of Aeronautics and Astronautics,2007,33(4):472-476. |
| |
| Authors: | Yao Shuzhen Jing Maozhong |
| |
| Institution: | School of Computer Science and Technology, Beijing University of Aeronautics and Astronautics, Beijing 100083, China |
| |
| Abstract: | |
| |
| Keywords: | model buildings Petri nets semantics analysis |
| 本文献已被 CNKI 维普 万方数据 等数据库收录！ |
| 点击此处可从《北京航空航天大学学报》浏览原始摘要信息 |
| 点击此处可从《北京航空航天大学学报》下载免费的PDF全文 |
|
