一种UML2.0模型动态特性的一致性验证方法

• 作者: 裴磐洁 雷博
• 来源期刊: 信息技术
• 学科: 工学
• 关键词: UML2.0 状态图 顺序图 一致性 模型检测
• 年，卷（期）: 2014,（8）
• 所属期刊栏目: 应用技术
• 页码范围: 183-186
• 页数: 4页
• 分类号: TP311.52
• 字数: 2488字
• 语种: 中文

摘要

近年来,UML已经被广泛应用于软件的分析和设计,然而,由于软件系统的复杂性,在UML模型中,难免会引入不同图表间特别是动态视图之间的不一致性.提出了一种用于验证UML2.O模型状态图和顺序图一致性的方法.首先,用XYZ/E来形式化描述状态图并将其转化为Promela输入语言;然后,用LTL来表示顺序图间的相互作用;最后利用模型检测工具Spin通过检查Promela描述的状态图是否满足LTL公式来达到检测模型一致性的目的.