面向模型检验的UML状态机语义
UML状态机(SM)是UML中用来对系统各种元素的离散行为建模的图.它丰富的表示符号提供了强大的描述机制,但也降低了其结构的模块性,提高了对其分析验证的难度.模型检验是自动检验有限状态并发系统的技术.通过模型检验SM描述的不同系统元素的行为是否满足某些性质,能尽早发现设计中的错误.为了将模型检验技术应用于SM的验证,本文用kripke结构定义SM的操作语义.与已有的SM语义定义不同,本文考虑到了SM中包含的不确定因素,用kripke结构描述系统所有可能的演化轨迹.通过检验从SM翻译得到的kripke结构达到模型检验SM的目的.
UML 操作语义 Kripke结构 模型检验 建模语言 状态机 软件工程
周颖 郑国梁 李宣东
南京大学计算机软件新技术国家重点实验室(南京);南京大学计算机科学技术系(南京)
国内会议
北京
中文
16-23
2003-11-01（万方平台首次上网日期，不代表论文的发表时间）