The Community for Technology Leaders
Green Image
Issue No. 12 - Dec. (2014 vol. 40)
ISSN: 0098-5589
pp: 1206-1223
Cong Tian , ICTT and ISN Laboratory, Xidian University, Xi’an, China
Zhenhua Duan , ICTT and ISN Laboratory, Xidian University, Xi’an, China
Zhao Duan , ICTT and ISN Laboratory, Xidian University, Xi’an, China
ABSTRACT
Counter-example guided abstraction refinement (CEGAR) is widely used in software model checking. With an abstract model, the state space is largely reduced, however, a counterexample found in such a model that does not satisfy the desired property may not exist in the concrete model. Therefore, how to check whether a reported counterexample is spurious is a key problem in the abstraction-refinement loop. Next, in the case that a spurious counterexample is found, the abstract model needs to be further refined where an NP-hard state separation problem is often involved. Thus, how to refine the abstract model efficiently has attracted a great attention in the past years. In this paper, by re-analyzing spurious counterexamples, a new formal definition of spurious paths is given. Based on it, efficient algorithms for detecting spurious counterexamples are presented. By the new algorithms, when dealing with infinite counterexamples, the finite prefix to be analyzed will be polynomially shorter than the one dealt with by the existing algorithms. Moreover, in practical terms, the new algorithms can naturally be parallelized that enables multi-core processors contributes more in spurious counterexample checking. In addition, a novel refining approach by adding extra Boolean variables to the abstract model is presented. With this approach, not only the NP-hard state separation problem can be avoided, but also a smaller refined abstract model can be obtained. Experimental results show that the new algorithms perform well in practice.
INDEX TERMS
Abstracts, Concrete, Model checking, Software, Color, Computational modeling, Benchmark testing
CITATION

C. Tian, Z. Duan and Z. Duan, "Making CEGAR More Efficient in Software Model Checking," in IEEE Transactions on Software Engineering, vol. 40, no. 12, pp. 1206-1223, 2014.
doi:10.1109/TSE.2014.2357442
173 ms
(Ver 3.3 (11022016))