一种新的statechart模型验证方法

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