首页 | 本学科首页   官方微博 | 高级检索  
     

一种新的Statechart模型验证方法
引用本文:陈丽娜,赵建民.一种新的Statechart模型验证方法[J].计算机科学,2011,38(2):144-147,165.
作者姓名:陈丽娜  赵建民
作者单位:浙江师范大学数理与信息工程学院,金华,321004
基金项目:本文受浙江省自然科学基金项目(Y1100689)资助。
摘    要:在传统的基于时序逻辑的模型检查框架下验证Statcchart模型面临三大挑战:全状态空间搜索、多次重复搜索和复杂时序逻辑公式难写。基于上述问题和实践工作,提出一种新的Statechart模型验证方法。该方法的中心是一种强化了的属性描述语言—属性状态图,并利用属性状态图中存在的先后关系和并发关系,把各个属性状态图有机地结合成一个树结构—属性树。属性树涵盖了目标系统要求验证的属性空间,因此可自上而下的验证整棵属性树。在验证过程中系统Statechart模型对应状态空间是逐步展开的,每验证部分属性就展开相应的部分状态空间并对其进行验证,验证过程是基于属性树转换并以step为单位,验证step的初始status和结束status是否满足对应属性树节点公式对其的属性约束,这样既能够迅速找出错误又能屏蔽step内部系统Statcchart模型的状态变化,使得验证过程更简单快捷。为了说明属性状态图和基于其的验证算法是实用和易用的,通过一个例子说明了从模型设计到具体验证整个过程。

关 键 词:状态图,模型检查,模型验证,时序逻辑,状态爆炸问题,形式化语义,反应系统

New Approach to Verify Statechart Models
CHEN Li-n,ZHAO Jian-min.New Approach to Verify Statechart Models[J].Computer Science,2011,38(2):144-147,165.
Authors:CHEN Li-n  ZHAO Jian-min
Affiliation:(College of Mathematics Physics and Information Engineering, Zhejiang Normal University, Jinhua 321004, China)
Abstract: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 languagcProperty Statechart. Using property statcchart, 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.
Keywords:Statechart  Model checking  Model verification  Temporal logic  State explosion problem  Formal semantics  Reactive systems
本文献已被 万方数据 等数据库收录!
点击此处可从《计算机科学》下载全文
设为首页 | 免责声明 | 关于勤云 | 加入收藏

Copyright©北京勤云科技发展有限公司  京ICP备09084417号