基于OBDD的SMC反例生成研究

计算机工程与应用 ›› 2012, Vol. 48 ›› Issue (10): 54-58.

基于OBDD的SMC反例生成研究

姚全珠，苗永军

西安理工大学计算机科学与工程学院，西安 710048

出版日期:2012-04-01 发布日期:2012-04-11

Counterexample generation research in symbolic model checking based on OBDD

YAO Quanzhu, MIAO Yongjun

School of Computer Science and Engineering, Xi’an University of Technology, Xi’an 710048, China

Online:2012-04-01 Published:2012-04-11

摘要/Abstract

摘要： 针对传统的符号模型检测反例生成算法在生成反例时会产生大量的无关变量，使得反例难以理解。提出一种改进的反例生成算法，将反例中的状态扩展为一个状态集，使用零压缩二叉决策图（Zero-Suppressed Binary Decision Diagrams，ZBDD）来存储所求出的状态集。删除了系统中的无关变量，仅保留了相关的变量，实验表明该算法能有效地减少状态的变量数，减少存储反例所需的空间。

关键词: 有序二叉决策图, 模型检测, 计算树逻辑（CTL）, 反例生成

Abstract: Because the traditional symbolic model checking for counterexample generation algorithm to generate counter-examples of a large amount of unrelated variables, making the counter-example is very difficult to understand. An improved counter-example generation algorithm, the state of the anti-expansion case, a state set calculated using zero-suppressed binary decision diagrams（ZBDD） is used to store the state set. Then delete the system independent variables, retain the relevant variables. Experiments show that the algorithm can effectively reduce the number of state variables and reduce the storage space required by counterexample.

Key words: Ordered Binary Decision Diagram（OBDD）, model checking, Computation Tree Logic（CTL）, counterexample generation

姚全珠，苗永军. 基于OBDD的SMC反例生成研究[J]. 计算机工程与应用, 2012, 48(10): 54-58.

YAO Quanzhu, MIAO Yongjun. Counterexample generation research in symbolic model checking based on OBDD[J]. Computer Engineering and Applications, 2012, 48(10): 54-58.

[1]	李茜1，王峥1，马建芬1，李娜2. 轻量级移动支付协议公平性分析[J]. 计算机工程与应用, 2018, 54(19): 82-87.
[2]	李前利，江华. 命题μ-演算局部模型检测高效算法设计[J]. 计算机工程与应用, 2017, 53(9): 51-56.
[3]	秦嫚蔓，王峥，王莉. 基于SPIN的远程证明协议的形式化分析及改进[J]. 计算机工程与应用, 2017, 53(1): 34-38.
[4]	吕江华1，刘志锋1，徐亚涛2，周从华1. 基于属性的访问控制策略的正确性验证[J]. 计算机工程与应用, 2016, 52(18): 98-103.
[5]	夏春蕊1，王瑞1，李晓娟1，关永1，张杰2，魏洪兴3. 动态环境下基于概率模型检测的路径规划方法[J]. 计算机工程与应用, 2016, 52(12): 5-11.
[6]	黄延凯，周宇，魏欧. 新型属性图文法反应式规约验证方法[J]. 计算机工程与应用, 2016, 52(12): 15-18.
[7]	王铭1，王瑞1，李晓娟1，关永1，张杰2，魏洪兴3. 非确定性环境中移动机器人避障策略的验证 ——基于形式化建模和概率分析[J]. 计算机工程与应用, 2016, 52(10): 31-38.
[8]	张舒青，徐中伟，陈祖希. 基于项重写系统的联锁系统模型检测方法研究[J]. 计算机工程与应用, 2014, 50(3): 49-54.
[9]	王昌达1，2，董雪刚1，周从华1，2. 基于UCON的网络银行在线支付及其安全性分析[J]. 计算机工程与应用, 2014, 50(16): 90-94.
[10]	佟超，王建新，齐建东. 基于形式化规约的缺陷规则库构建与检测方法[J]. 计算机工程与应用, 2014, 50(13): 66-72.
[11]	尤启房，杨晋吉. SIP协议的SPIN模型检测[J]. 计算机工程与应用, 2014, 50(13): 87-89.
[12]	吕威，黄志球，陈哲，阚双龙，魏欧. ESpin*：基于SPIN的Eclipse模型检测环境[J]. 计算机工程与应用, 2013, 49(7): 45-51.
[13]	陈娟娟，魏欧，黄志球，陈哲. 基于双格的多值模型的精化关系与对称化简[J]. 计算机工程与应用, 2013, 49(22): 40-45.
[14]	缪力，谭志华，张大方. 基于SPIN的网络认证协议高效模型检测[J]. 计算机工程与应用, 2012, 48(21): 62-67.
[15]	郝身刚，张丽. 有界模型检测在服务组合中的应用研究[J]. 计算机工程与应用, 2012, 48(10): 111-114.