Combining Symmetry Reduction and Under-Approximation for Symbolic Model Checking
Combining Symmetry Reduction and Under-Approximation for Symbolic Model Checking
复制标题
结合对称性约简和欠近似进行符号模型检查
DOI：
--
复制
发表时间：
2002
期刊：
影响因子：
--
通讯作者：
O. Grumberg
中科院分区：
文献类型：
--
作者：
S. Barner;O. Grumberg
这项工作提出了一个集合的方法，集成了简化和欠近似与符号模型检查，以减少空间和时间。这些方法的主要目的是伪造。然而，在某些条件下，他们可以提供验证，以及。我们首先提出的算法，使用对称性约简执行的飞行模型检查的时间安全属性。这些算法避免了建立轨道关系，在计算可达状态时选择代表。然后，我们扩展这些算法来检查活性属性。此外，我们引入了一个迭代的飞行算法，建立子集的轨道关系，而不是完整的relations.Our方法是完全自动的，一旦用户提供一些基本信息的对称性验证系统。此外，即使用户提供的信息不正确，这些方法也是鲁棒的并且正确地工作。此外，该方法返回正确的结果，即使当对称性约简的计算尚未完成，由于内存或时间explosion.We实现我们的方法在IBM模型检查器Rule-Base和比较其性能的RuleBase。在大多数情况下，我们的算法在时间和空间上都优于RuleBase。
This work presents a collection of methods that integrate symmetryreduction and under-approximation with symbolic model checking in order to reduce space and time. The main objective of these methods is falsification. However, under certain conditions, they can provide verification as well.We first present algorithms that use symmetry reduction to perform on-the-fly model checking for temporal safety properties. These algorithms avoid building the orbit relation and choose representatives on-the-fly while computing the reachable states. We then extend these algorithms to check liveness properties as well. In addition, we introduce an iterative on-the-fly algorithm that builds subsets of the orbit relation rather than the full relation.Our methods are fully automatic once the user supplies some basic information about the symmetry in the verified system. Moreover, the methods are robust and work correctly even if the information supplied by the user is incorrect. Furthermore, the methods return correct results even when the computation of the symmetry reduction has not been completed due to memory or time explosion.We implemented our methods within the IBM model checker Rule-Base and compared their performance to that of RuleBase. In most cases, our algorithms outperformed RuleBase in both time and space.