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

维普资讯 2007年 4月 北 京 航 空 航 天 大 学 学 报 April 2007 第33卷 第4期 JournalofBeijingUniversityofAeronauticsandAstronautics Vo1．33 No．4 UML状态图的形式化建模及其分析 姚淑珍 金茂忠 (北京航空航天大学 计算机学院，北京 100083) 摘 要：为解决状态图的建模 问题，特别是带有复合状态的层次化状态 图的建模 问 题 ，分析了UML状态 图的结构特点和语义特征，构造了层次化着色Petri网HCPN．将复合状态 的Petri网子网结构划分成输入／输出端 口、状态迁移部分和历史状态部分．其 中输入 ／输 出端 口分别用于完成子网进入弧的解析和离开的弧的汇总，状态迁移部分完成状态机子网内部状 态变换，历史状态部分通过 “记忆单元”，完成复合状态的 “记忆恢复”和 “记忆刷新”．基于所 构造的HCPN结构，总结 了状态图复合状态转入 ／转 出迁移 的语义和约束规则，阐述 了复合状 态的Petri网子网的相应描述方法和分析技术．最后针对状态图的安全性要求详细论述 了历史 状态完备性判定原则、父子层一致性判定原则和状态可达性判定原则的HCPN语义表示．研究 成果对进一步开发 自动化分析验证工具 ，优化复杂系统设计方案，提高软件质量具有重要的指 导意义． 关 键 词：建模 ；Petri网；语义；分析 中图分类号：TP311．5 文献标识码：A 文 章 编 号：1001—5965(2007)04-0472—05 FOrmalmodelingandanalysisofUMLstatecharts YaoShuzhen JingMaozhong (SchoolofComputerScienceandTechnology，BeijingUniversityofAeronauticsandAstronautics，Beijing100083，China) Abstract：ThestructuralandsemanticfeaturesofUMLstatechartsareanalyzedfirstly，andthehierarchi— calcoloredPetrinet(HCPN)isconsturctedtosolvemodelingissues，especiallythoserelatedtohierarchical statechartswithcompositestates．ThePetrisubnetfora compositestateiscomposed ofinput／outputinter— faces，astate—transitionpartandahistorystatepart．Theinput／outputinterfacesareusedtoparseentry arcs andgatherexitingarcsto／from compositesrespectively．Thestate—transitionpartrealizestransitionsofthein— ternalstates．Thehistory statepartdealswithmemory recovery andmemory cleanupofhistory units．Afterab— stractingsemanticurlesandconstrainsofentry ／exittransitions，theirdescriptionsandanalysistechniquesof compositestatesbasedonHCPNsareillustrated．Finally，intheview