Parallel Multiple Counter-Examples Guided Abstraction Loop — Applying to Timed Automaton

DOI：

发表时间：

2016

期刊：

影响因子：

通讯作者：

中科院分区：

其他

文献类型：

作者：

Kozo Okano;Takeshi Nagaoka;Toshiaki Tanaka;Toshifusa Sekizawa;S. Kusumoto

模型检测技术通过穷举搜索代表系统整体行为的有限迁移系统来证明给定系统满足给定规范。如果系统变得很大，则由于所使用的CPU时间和存储模型的内存空间，不可能在合理的时间内探索整个状态。这就是所谓的状态爆炸问题。避免状态爆炸问题的解决方案之一是使用模型抽象技术。通常，从原始模型构造这样的抽象模型变得容易出错。为此，本文研究了抽象模型的自动生成技术。尤其是反例引导的抽象精化（CEGAR）被认为是一种很有前途的技术，因为它从一个小的抽象模型开始，如果结果是虚假的，它会自动精化抽象模型。我们已经为时间自动机提出了一个具体的CEGAR循环。该迭代循环在细粒度级别上细化模型。它避免了状态爆炸，但是，循环的数量增加了。本文提出了一种改进的技术，其中多个反例同时适用于CEGAR的细化步骤。该装置减少了迭代循环的数量。实验结果表明了该方法的有效性。

A model checking technique proves that a given system satisfies given specifications by searching exhaustively a finite transition system which represents the system’s whole behavior. If the system becomes large, it is impossible to explore the whole states in reasonable time due to both of CPU time used and memory space where the model is stored. This is called the state explosion problem. One of the solutions to avoid the state explosion problem is using a model abstraction technique. In usual, constructing such an abstract model from the original model becomes error-prone. Hence, automatic generation techniques of abstract models are studied. Especially, Counter-Example Guided Abstraction Refinement (CEGAR) is considered as a promising technique because it automatically refines abstract model if the result is spurious, starting from a small abstract model. We have already proposed a concrete CEGAR loop for a timed automaton. This iteration loop refines the model in fine granularity level. It avoids the state explosion, however, the number of loops increases. This paper proposes a revised technique where multiple counter-examples are simultaneously applied in the refinement step of CEGAR. This device reduces the number of iteration loops. Experimental results show the improvement.

Parallel Multiple Counter-Examples Guided Abstraction Loop — Applying to Timed Automaton—

文献摘要

相似文献