UML类图的形式规约与精化研究

• 作者: 杨宗源 王博文 盛枫 窦亮
• 来源期刊: 计算机应用与软件
• 学科: 工学
• 关键词: UML类图 模型精化 Coq机械语意
• 年，卷（期）: 2017,（2）
• 所属期刊栏目: 软件技术与研究
• 页码范围: 1-7,47
• 页数: 8页
• 分类号: TP301.2
• 字数: 4894字
• 语种: 中文
• DOI: 10.3969/j.issn.1000-386x.2017.02.001

摘要

UML由于其广泛的应用和直观的图形化符号,成为了模型驱动工程的重要组成部分.但UML本身缺乏精确的形式语义定义,缺少对其模型精化关系的形式化规范定义,对UML模型进行形式验证变得尤为困难.UML类图作为描述系统结构的静态模型,不具备完整的形式语义.从UML类图的机械语义中抽取出形式规约,将UML类图中的结构和形式规约转换成定理证明器Coq中的机械语义定义.此外,还提出了类图的结构精化操作,将模型间的精化关系在Coq中进行形式化定义,并且对精化操作的原子操作进行机械验证,保证其精化前后系统的结构和语义保持一致.将UML和形式化方法相结合,为可验证的软件设计精化框架提供了理论依据.

作者信息

序号	姓名	单位	发文数	被引次数	H指数	G指数
1	杨宗源	华东师范大学信息科学技术学院	32	326	9.0	17.0
2	窦亮	华东师范大学信息科学技术学院	10	73	5.0	8.0
3	王博文	华东师范大学信息科学技术学院	2	33	2.0	2.0
4	盛枫	华东师范大学信息科学技术学院	2	15	1.0	2.0