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

被引：9

作者：

姚淑珍

金茂忠

机构：

[1] 北京航空航天大学计算机学院

来源：

北京航空航天大学学报 | 2007年 / 04期

关键词：

建模; Petri网; 语义; 分析;

D O I：

10.13700/j.bh.1001-5965.2007.04.022

中图分类号：

TP311.52 [];

学科分类号：

081202 ; 0835 ;

摘要：

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

引用

页码：472 / 476

页数：5