基于模型检测的UML状态图和顺序图一致性检测

›› 2012, Vol. 25 ›› Issue (2): 100-.

基于模型检测的UML状态图和顺序图一致性检测

杜杰,江国华

(南京航空航天大学计算机科学与技术学院,江苏南京 210016)

出版日期:2012-02-15 发布日期:2012-02-29
作者简介:杜杰(1987—),女,硕士研究生。研究方向:软件测试。江国华(1963—),男,副教授,硕士生导师。研究反方向:软件工程,软件测试。

Consistency Check Between UML State Chart and Sequence Chart Based on Model Checking

DU Jie, JIANG Guo-Hua

(School of Computer Science and Technology,Nanjing University of Aeronautics and Astronautics,Nanjing 210016,China)

Online:2012-02-15 Published:2012-02-29

摘要/Abstract

摘要：

用户可使用UML从不同角度对系统进行建模,但不同视图间存在信息冗余,会导致视图不一致的问题。文中提出形式化与可视化UML互补建模的方法,探讨用模型检测验证UML模型中的状态图和顺序图的一致性问题。针对具有复合片段的顺序图提出分析方法,将复杂层次结构的状态图转换为有限状态机,再用模型检测工具NuSMV对建立的模型进行验证。最后通过实例对此转换方法进行验证,实验结果表明了此方法的有效性。

关键词: UML, 模型检测, NuSMV

Abstract:

UML can be used to accomplish the system modeling from different views.There may be some redundancy in different views,so that the views may be inconsistent.This paper proposes modeling methods based on the formalization method and the UML.It focuses mainly on using the model checking to check the consistency between the UML statechart and the sequence chart.The method to deal with the composite sequence chart is proposed and the hierarchy structure of the statechart is translated into the finite automata machine.Then the NuSMV is used to verify them.Experimental results show the effectiveness of the converting methods.

Key words: UML;model checking;NuSMV

中图分类号:

TP311.55

杜杰, 江国华. 基于模型检测的UML状态图和顺序图一致性检测[J]. , 2012, 25(2): 100-.

DU Jie, JIANG Guo-Hua. Consistency Check Between UML State Chart and Sequence Chart Based on Model Checking[J]. , 2012, 25(2): 100-.

[1]	张洁. 一种复杂系统定性模型描述方法[J]. , 2014, 27(4): 34-.
[2]	黄超, 江国华. 一种Ada并发程序的模型检测方法[J]. , 2012, 25(3): 44-.
[3]	顾炜, 黄志球, 李剑. UML活动图到时间Petri网的映射方法[J]. , 2012, 25(2): 105-.
[4]	陶乃利, 刘文波. 基于UML自动测试系统软件面向对象建模[J]. , 2011, 24(2): 92-.
[5]	薛媛. 基于UML的考试管理系统设计[J]. , 2011, 24(12): 19-.