面向模型检验的UML状态机语义

• 作者: 周颖 李宣东 郑国梁
• 来源期刊: 电子学报
• 学科: 工学
• 关键词: UML 状态机 操作语义 Kripke结构 模型检验
• 年，卷（期）: 2003,（z1）
• 所属期刊栏目: 信息处理技术
• 页码范围: 2091-2095
• 页数: 5页
• 分类号: TP311
• 字数: 6134字
• 语种: 中文
• DOI: 10.3321/j.issn:0372-2112.2003.z1.034

摘要

UML状态机(SM)是UML中用来对系统各种元素的离散行为建模的图.它丰富的表示符号提供了强大的描述机制,但也降低了其结构的模块性,提高了对其分析验证的难度.模型检验是自动检验有限状态并发系统的技术.通过模型检验SM描述的不同系统元素的行为是否满足某些性质,能尽早发现设计中的错误.为了将模型检验技术应用于SM的验证,本文用kripke结构定义SM的操作语义.与已有的SM语义定义不同,本文考虑到了SM中包含的不确定因素,用kripke结构描述系统所有可能的演化轨迹.通过检验从SM翻译得到的kripke结构达到模型检验SM的目的.

作者信息

序号	姓名	单位	发文数	被引次数	H指数	G指数
1	李宣东	南京大学计算机软件新技术国家重点实验室	72	1417	20.0	36.0
5	郑国梁	南京大学计算机软件新技术国家重点实验室	77	1523	21.0	37.0
9	周颖	南京大学计算机软件新技术国家重点实验室	9	190	6.0	9.0