共 1 条
面向模型检验的UML状态机语义
被引：8
作者：
周颖
郑国梁
李宣东
机构：
[1] 南京大学计算机软件新技术国家重点实验室
[2] 南京大学计算机科学技术系 江苏南京
[3] 江苏南京
来源：
关键词：
UML;
状态机;
操作语义;
Kripke结构;
模型检验;
D O I：
暂无
中图分类号：
TP312 [程序语言、算法语言];
学科分类号：
081202 ;
0835 ;
摘要：
UML状态机 (SM)是UML中用来对系统各种元素的离散行为建模的图 .它丰富的表示符号提供了强大的描述机制 ,但也降低了其结构的模块性 ,提高了对其分析验证的难度 .模型检验是自动检验有限状态并发系统的技术 .通过模型检验SM描述的不同系统元素的行为是否满足某些性质 ,能尽早发现设计中的错误 .为了将模型检验技术应用于SM的验证 ,本文用kripke结构定义SM的操作语义 .与已有的SM语义定义不同 ,本文考虑到了SM中包含的不确定因素 ,用kripke结构描述系统所有可能的演化轨迹 .通过检验从SM翻译得到的kripke结构达到模型检验SM的目的
引用
收藏
页码：2091 / 2095
页数：5
相关论文