摘要
在传统的基于时序逻辑的模型检查框架下验证Statechart模型面临三大挑战:全状态空间搜索、多次重复搜索和复杂时序逻辑公式难写。基于上述问题和实践工作,提出一种新的Statechart模型验证方法。该方法的中心是一种强化了的属性描述语言———属性状态图,并利用属性状态图中存在的先后关系和并发关系,把各个属性状态图有机地结合成一个树结构———属性树。属性树涵盖了目标系统要求验证的属性空间,因此可自上而下的验证整棵属性树。在验证过程中系统Statechart模型对应状态空间是逐步展开的,每验证部分属性就展开相应的部分状态空间并对其进行验证,验证过程是基于属性树转换并以step为单位,验证step的初始status和结束status是否满足对应属性树节点公式对其的属性约束,这样既能够迅速找出错误又能屏蔽step内部系统Statechart模型的状态变化,使得验证过程更简单快捷。为了说明属性状态图和基于其的验证算法是实用和易用的,通过一个例子说明了从模型设计到具体验证整个过程。
The traditional temporal logic based Statechart model checking faces three challenges：global state space search,multipass search and writing correct temporal properties.To attack these problems,a new approach to verify Statechart models was introduced in this paper.The core of this approach is a strengthened property specification language-Property Statechart.Using property statechart,the runs of Statechart models and their consisting status were defined clearly and detailedly.Before verification,property statecharts were reconstructed into one big property tree based on the before-and-after and concurrent relationships among them.This property tree covers all the properties of target Statechart models needed to verify.In the process of verification,the state space of Statechart models is unfolded step by step.To verify a part of properties we only need to search part of state space instead of the whole state space and make sure that the statuses included by this part of state space meet the propositions specified in the corresponding nodes in the property tree.So the verification can be more efficient.Then we discussed how to verify deterministic reactive systems and non-deterministic reactive systems using our ideas.A case study illustrates the approach presented in this paper.
出处
《计算机科学》
CSCD
北大核心
2011年第2期144-147,165,共5页
Computer Science
基金
浙江省自然科学基金项目(Y1100689)资助
关键词
状态图
模型检查
模型验证
时序逻辑
状态爆炸问题
形式化语义
反应系统
Statechart
Model checking
Model verification
Temporal logic
State explosion problem
Formal semantics
Reactive systems
