面向模型检验的UML状态机语义 |
| |
作者姓名: | 周颖 郑国梁 李宣东 |
| |
作者单位: | [1]南京大学计算机软件新技术国家重点实验窒,江苏南京210093 [2]南京大学计算机科学技术系.江苏南京210093 |
| |
摘 要: | UML状态机(SM)是UML中用来对系统各种元素的离散行为建模的图.它丰富的表示符号提供了强大的描述机制,但也降低了其结构的模块性,提高了对其分析验证的难度.模型检验是自动检验有限状态并发系统的技术.通过模型检验SM描述的不同系统元素的行为是否满足某些性质,能尽早发现设计中的错误.为了将模型检验技术应用于SM的验证,本文用kripke结构定义SM的操作语义.与已有的SM语义定义不同,本文考虑到了SM中包含的不确定因素,用kripke结构描述系统所有可能的演化轨迹、通过检验从SM翻译得到的kripke结构达到模型检验SM的目的.
|
关 键 词: | UML 状态机 操作语义 Kripke结构 模型检验 |
本文献已被 维普 等数据库收录! |
|