摘要
UML状态机 (SM)是UML中用来对系统各种元素的离散行为建模的图 .它丰富的表示符号提供了强大的描述机制 ,但也降低了其结构的模块性 ,提高了对其分析验证的难度 .模型检验是自动检验有限状态并发系统的技术 .通过模型检验SM描述的不同系统元素的行为是否满足某些性质 ,能尽早发现设计中的错误 .为了将模型检验技术应用于SM的验证 ,本文用kripke结构定义SM的操作语义 .与已有的SM语义定义不同 ,本文考虑到了SM中包含的不确定因素 ,用kripke结构描述系统所有可能的演化轨迹 .
The state machine formalism in UML is used for modeling discrete behavior of various system elements.Its rich notation provides a powerful description mechanism which meanwhile decreases modality of its structure and increases verifying complexity.Model checking is a technique for automatically verifying finite-state concurrent systems.By model checking the behavior of various system elements described by SM,we can find design errors as soon as possible.This paper defines an operational semantics for SM using Kripke structure in order to model checking SM.Different from existing SM semantics definitions,this paper takes undetermined factors in SM into consideration .SM is translated into kripke structure that describes all possible evolving traces on which model checker checks.
出处
《电子学报》
EI
CAS
CSCD
北大核心
2003年第z1期2091-2095,共5页
Acta Electronica Sinica
基金
8 63项目 (No.2 0 0 1AA1 1 32 0 3
No .2 0 0 2AA1 1 60 90 )
自然科学基金项目 (No.60 2 0 70 36)
973项目 (No .2 0 0 2CB31 2 0 0 1 )
