Managing space for finite-state verification
Managing space for finite-state verification
复制标题
DOI：
10.1145/1134285.1134308
复制
发表时间：
2006-05
期刊：
影响因子：
--
通讯作者：
Jianbin Tan;G. Avrunin;L. Clarke
中科院分区：
文献类型：
--
作者：
Jianbin Tan;G. Avrunin;L. Clarke
有限状态验证（FSV）技术试图通过检查系统模型的所有可能行为来证明该模型的属性。这种方法受到状态爆炸问题的困扰，其中模型的大小或分析成本可能相对于系统的大小呈指数级增长。使用符号数据结构来表示状态空间的子集已被证明通常是硬件验证的有效优化方法。然而，软件验证的价值仍然不清楚。在本文中，我们研究了两种符号数据结构，二进制决策图（bdd）和零抑制二进制决策图（zdd）在两个FSV工具LTSA和FLAVERS中的应用。我们描述了一个实验，表明这两种符号方法可以提高FSV工具的性能，并且比其他两种显式存储状态空间的算法更有效。此外，基于zdd的方法通常比基于bdd的方法运行得更快，可以处理更大的系统。
Finite-state verification (FSV) techniques attempt to prove properties about a model of a system by examining all possible behaviors of that model. This approach suffers from the state-explosion problem, where the size of the model or the analysis costs may be exponentially large with respect to the size of the system. Using symbolic data structures to represent subsets of the state space has been shown to usually be an effective optimization approach for hardware verification. The value for software verification, however, is still unclear. In this paper, we investigate applying two symbolic data structures, Binary Decision Diagrams (BDDs) and Zero-suppressed Binary Decision Diagrams (ZDDs), in two FSV tools, LTSA and FLAVERS. We describe an experiment showing that these two symbolic approaches can improve the performance of both FSV tools and are more efficient than two other algorithms that store the state space explicitly. Moreover, the ZDD-based approach often runs faster and can handle larger systems than the BDD-based approach.