基于OBDD的SMC反例生成研究  

Counterexample generation research in symbolic model checking based on OBDD

作　　者：姚全珠[1] 苗永军[1] 

机构地区：[1]西安理工大学计算机科学与工程学院,西安710048

出　　处：《计算机工程与应用》2012年第10期54-58,145,共6页Computer Engineering and Applications

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

关 键 词：有序二叉决策图 模型检测 计算树逻辑(CTL) 反例生成 

分 类 号：TP311[自动化与计算机技术—计算机软件与理论]