| 面向模型检验的UML状态机语义 |
| |
| 引用本文： | 周颖,郑国梁,李宣东.面向模型检验的UML状态机语义[J].电子学报,2003,31(Z1):2091-2095. |
| |
| 作者姓名： | 周颖 郑国梁 李宣东 |
| |
| 作者单位： | 1. 南京大学计算机软件新技术国家重点实验室, 江苏, 南京, 210093;
2. 南京大学计算机科学技术系, 江苏, 南京, 210093 |
| |
| 基金项目： | 国家高技术研究发展计划(863计划)，国家自然科学基金，国家重点基础研究发展计划(973计划)，2001AA113203,2002AA116090，60207036，2002CB312001，，， |
| |
| 摘 要： | UML状态机(SM)是UML中用来对系统各种元素的离散行为建模的图.它丰富的表示符号提供了强大的描述机制,但也降低了其结构的模块性,提高了对其分析验证的难度.模型检验是自动检验有限状态并发系统的技术.通过模型检验SM描述的不同系统元素的行为是否满足某些性质,能尽早发现设计中的错误.为了将模型检验技术应用于SM的验证,本文用kripke结构定义SM的操作语义.与已有的SM语义定义不同,本文考虑到了SM中包含的不确定因素,用kripke结构描述系统所有可能的演化轨迹.通过检验从SM翻译得到的kripke结构达到模型检验SM的目的.
|
| 关 键 词： | UML 状态机 操作语义 Kripke结构 模型检验 |
| 文章编号： | 0372-2112(2003)12A-2091-05 |
| 收稿时间： | 2003-09-30 |
| 修稿时间： | 2003年9月30日 |
An Operational Semantics for UML State Machines in Model Checking Context |
| |
| ZHOU Ying,ZHENG Guo-liang,LI Xuan-dong.An Operational Semantics for UML State Machines in Model Checking Context[J].Acta Electronica Sinica,2003,31(Z1):2091-2095. |
| |
| Authors: | ZHOU Ying ZHENG Guo-liang LI Xuan-dong |
| |
| Affiliation: | 1. State Key Laboratory for Novel Software Technology, Nanjing University, Nanjing, Jiangsu 210093, China;
2. Department of Computer Science and Technology, Nanjing University, Nanjing, Jiangsu 210093, China |
| |
| Abstract: | |
| |
| Keywords: | UML |
| 本文献已被 万方数据 等数据库收录！ |
| 点击此处可从《电子学报》浏览原始摘要信息 |
|
点击此处可从《电子学报》下载全文 |
|
