一种新的Statechart模型验证方法

• 作者: 赵建民 陈丽娜
• 来源期刊: 计算机科学
• 学科: 工学
• 关键词: 状态图 模型检查 模型验证 时序逻辑 状态爆炸问题 形式化语义 反应系统
• 年，卷（期）: 2011,（2）
• 页码范围: 144-147,165
• 分类号: TP302
• 字数: 5339字
• 语种: 中文
• DOI: 10.3969/j.issn.1002-137X.2011.02.033

摘要

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

作者信息

序号	姓名	单位	发文数	被引次数	H指数	G指数
1	赵建民	浙江师范大学数理与信息工程学院	121	1027	18.0	25.0
2	陈丽娜	浙江师范大学数理与信息工程学院	17	88	5.0	9.0