元模型层次的 UML 动态子图到 Coq 形式规范的转换

• 作者: 尹敏 李超 杨宗源 窦亮
• 来源期刊: 计算机应用与软件
• 学科: 工学
• 关键词: UML 动态子图 模型转换 元模型 Coq Kermeta
• 年，卷（期）: 2016,（8）
• 所属期刊栏目: 软件技术与研究
• 页码范围: 7-11,66
• 页数: 6页
• 分类号: TP311
• 字数: 4564字
• 语种: 中文
• DOI: 10.3969/j.issn.1000-386x.2016.08.002

摘要

UML 动态子图主要包括序列图和状态图等，它们在描述系统的行为方面应用广泛，但是半形式化的语义使它们不能直接进行形式化验证。Coq 是目前主流的交互式定理证明器，用形式化的 Coq 规范来描述 UML 动态子图模型，可以在此基础上进行对模型的属性进行验证等工作。基于现有工作，提出将 UML 动态子图模型转换为 Coq 形式规范的框架，在元模型层次给出状态图和序列图的转换规则，介绍算法和原型工具实现。这种元模型层次的转换方法，保证了转换前后的语法正确性，为进一步分析验证提供了基础。

作者信息

序号	姓名	单位	发文数	被引次数	H指数	G指数
1	李超	华东师范大学计算机科学技术系	15	35	4.0	5.0
2	杨宗源	华东师范大学计算机科学技术系	32	326	9.0	17.0
3	窦亮	华东师范大学计算机科学技术系	10	73	5.0	8.0
4	尹敏	华东师范大学计算机科学技术系	3	18	2.0	3.0