| 一种UML状态图模型检测方法 |
| |
| 引用本文： | 张涛,黄少滨,黄宏涛,吕天阳,刘刚. 一种UML状态图模型检测方法[J]. 哈尔滨工程大学学报, 2011, 0(8): 1035-1039 |
| |
| 作者姓名： | 张涛 黄少滨 黄宏涛 吕天阳 刘刚 |
| |
| 作者单位： | 哈尔滨工程大学计算机科学与技术学院; |
| |
| 基金项目： | 国家自然科学基金资助项目(60873038,60903080); 中央高校基本科研业务专项资金项目(100603) |
| |
| 摘 要： | 为在开发过程早期发现系统设计的各种错误与不一致,提出一种UML状态图模型检测方法,用于验证设计模型与需求规约间的一致性.该方法通过元组定义UML状态图的主要元素,给出状态图的中间表示形式SC.基于SC上定义的操作语义,该方法将状态图转换为具有KRIPKE语义结构的状态迁移系统,并将系统需满足的性质表示为线性时序逻辑公式...
|
| 关 键 词： | 模型检测 迁移系统 操作语义 UML 状态图 |
A method for model checking UML statecharts |
| |
| ZHANG Tao,HUANG Shaobin,HUANG Hongtao,Lü Tianyang,LIU Gang. A method for model checking UML statecharts[J]. Journal of Harbin Engineering University, 2011, 0(8): 1035-1039 |
| |
| Authors: | ZHANG Tao HUANG Shaobin HUANG Hongtao Lü Tianyang LIU Gang |
| |
| Affiliation: | ZHANG Tao,HUANG Shaobin,HUANG Hongtao,Lü Tianyang,LIU Gang (College of Computer Science and Technology,Harbin Engineering University,Harbin 150001,China) |
| |
| Abstract: | The aim of this paper is to find various errors and inconsistencies of system design in the early stages of the development process.A method for model checking UML statecharts was proposed,and was used to verify the consistency of the design model and the requirement specifications.The elements of UML statecharts were defined by a tuple system,and the middle representation of the UML statecharts-SC-was given.Based on the definition of operational semantics of SC,the statechart was converted into a state tra... |
| |
| Keywords: | model checking transition system operational semantics UML statecharts |
| 本文献已被 CNKI 等数据库收录！ |
|
