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