%0 Journal Article
%T 一种新的statechart模型验证方法
%A 陈丽娜
%A 赵建民？
%J 计算机科学
%D 2011
%X 在传统的基于时序逻辑的模型检查框架下验证statcchart模型面临三大挑战:全状态空间搜索、多次重复搜索和复杂时序逻辑公式难写。基于上述问题和实践工作，提出一种新的statechart模型验证方法。该方法的中心是一种强化了的属性描述语言—属性状态图，并利用属性状态图中存在的先后关系和并发关系，把各个属性状态图有机地结合成一个树结构—属性树。属性树涵盖了目标系统要求验证的属性空间，因此可自上而下的验证整棵属性树。在验证过程中系统statechart模型对应状态空间是逐步展开的，每验证部分属性就展开相应的部分状态空间并对其进行验证，验证过程是基于属性树转换并以step为单位，验证step的初始status和结束status是否满足对应属性树节点公式对其的属性约束，这样既能够迅速找出错误又能屏蔽step内部系统statcchart模型的状态变化，使得验证过程更简单快捷。为了说明属性状态图和基于其的验证算法是实用和易用的，通过一个例子说明了从模型设计到具体验证整个过程。
%K 状态图
%K 模型检查
%K 模型验证
%K 时序逻辑
%K 状态爆炸问题
%K 形式化语义
%K 反应系统
%U http://www.jsjkx.com/jsjkx/ch/reader/view_abstract.aspx?file_no=110233&flag=1