Abstract
A heuristic-based symbolic model checking algorithm, BDD-IDA*. that efficiently falsifies invariant properties of a system is presented. As in bounded model checking, the algorithm uses an iterative deepening search strategy. However, in our case, the search strategy is guided by a heuristic that is computed from an abstract model, which is derived from the concrete model by a synthesis technique. Synthesis involves eliminating so-called weak variables from the concrete specification, where the weak variables are identified by a data-dependency analysis. Unique to this work is the use of the depth-first IDA* search algorithm in a BDD setting, and the automatic synthesis of the heuristic. The performance of the approach on a large number of small examples is compared with standard BDD-based approaches. Experiments on a variety of real-world models from different domains are also conducted. The approach reveals a consistent improvement on all models, and in some cases a speed-up of 2 orders of magnitude is obtained.
Chapter PDF
Similar content being viewed by others
Keywords
References
Biere, A., Cimatti, A., Clarke, E., Zhu, Y.: Symbolic model checking without bDDs. In: Cleaveland, W.R. (ed.) TACAS 1999. LNCS, vol. 1579, pp. 193–207. Springer, Heidelberg (1999)
Bryant, R.E.: Graph-based algorithms for Boolean function manipulation. IEEE Transaction C-35(8), 677–691 (1986)
Cabodi, G., Nocco, S., Quer, S.: Mixing forward and backward traversals in guided-prioritized BDD-based verification. In: Brinksma, E., Larsen, K.G. (eds.) CAV 2002. LNCS, vol. 2404, pp. 471–484. Springer, Heidelberg (2002)
Cimatti, A., Clarke, E., Giunchiglia, F., Roveri, M.: NUSMV: A new symbolic model verifier. In: Halbwachs, N., Peled, D.A. (eds.) CAV 1999. LNCS, vol. 1633, pp. 495–499. Springer, Heidelberg (1999)
Clarke, E., Gupta, A., Kukula, J., Strichman, O.: SAT based abstraction-refinement using ILP and machine learning techniques. In: Brinksma, E., Larsen, K.G. (eds.) CAV 2002. LNCS, vol. 2404, pp. 265–279. Springer, Heidelberg (2002)
Clarke, E.M., Grumberg, O., Long, D.E.: Model checking and abstraction. ACM Transactions on Programming Languages and Systems 16(5), 1512–1542 (1994)
Clarke, E.M., Grumberg, O., Peled, D.A.: Model Checking. MIT Press, Cambridge (1999)
Culberson, J.C., Schaeffer, J.: Searching with pattern databases. In: McCalla, G.I. (ed.) Canadian AI 1996. LNCS, vol. 1081, pp. 402–416. Springer, Heidelberg (1996)
Edelkamp, S., Lluch Lafuente, A., Leue, S.: Directed explicit model checking with HSF-SPIN. In: Dwyer, M.B. (ed.) SPIN 2001. LNCS, vol. 2057, pp. 57–79. Springer, Heidelberg (2001)
Edelkamp, S., Leue, S., Lluch-Lafuente, A.: Directed explicit-state model checking in the validation of communication protocols. Technical report, Albert-Ludwigs-Universitt Freiburg (2001)
Edelkamp, S., Lluch-Lafuente, A.: Abstraction databases in theory and model checking practice. In: Proceedings of Workshop on Connecting Planning Theory with Practice, International Conference on Automated Planning and Scheduling (ICAPS), Whistler, Canada (2004)
Fraer, R., Kamhi, G., Ziv, B., Vardi, M.Y., Fix, L.: Prioritized traversal: Efficient reachability analysis for verification and falsification. In: Emerson, E.A., Sistla, A.P. (eds.) CAV 2000. LNCS, vol. 1855, pp. 389–402. Springer, Heidelberg (2000)
Korf, R.: Iterative-deepening A*: An optimal admissible tree search. In: Ninth International Joint Conference on Artificial Intelligence(IJCAI-1985), LA, California, USA, pp. 1034–1036. Morgan Kaufmann, San Francisco (1985)
Korf, R.: Linear-space best-first search. Artificial Intelligence 62(1), 41–78 (1993)
McMillan, K.L.: Symbolic model checking. Kluwer Academic Publishers, Boston (1993)
Qian, K., Nymeyer, A.: Abstraction-based model checking using heuristical refinement. In: Wang, F. (ed.) ATVA 2004. LNCS, vol. 3299, pp. 165–178. Springer, Heidelberg (2004)
Qian, K., Nymeyer, A.: Guided invariant model checking based on abstraction and symbolic pattern databases. In: Jensen, K., Podelski, A. (eds.) TACAS 2004. LNCS, vol. 2988, pp. 497–511. Springer, Heidelberg (2004)
Ravi, K., Somenzi, F.: High-density reachability analysis. In: ICCAD 1995: Proceedings of the 1995 IEEE/ACM International Conference on Computer-Aided Design, pp. 154–158. IEEE Computer Society Press, Los Alamitos (1995)
Santone, A.: Heuristic search + local model checking in selective mu-calculus. IEEE Transactions on Software Engineering 29(6), 510–523 (2003)
Seppi, K., Jones, M., Lamborn, P.: Guided model checking with a bayesian meta-heuristic. In: Proceedings of the Fourth International Conference on Application of Concurrency to System Design (ACSD 2004), pp. 217–226. IEEE Computer Society Press, Los Alamitos (2004)
Tan, J., Avrunin, G.S., Clarke, L.A., Zilberstein, S., Leue, S.: Heuristic-guided counterexample search in flavers. In: SIGSOFT 2004/FSE-12: Proceedings of the 12th ACM SIGSOFT Twelfth International Symposium on Foundations of Software Engineering, pp. 201–210. ACM Press, New York (2004)
Yang, C.H., Dill, D.L.: Validation with guided search of the state space. In: Proceedings of the 35th Conference on Design Automation, Moscone Center, San Francico, California, USA, June 15-19, pp. 599–604. ACM Press, New York (1998)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2005 IFIP International Federation for Information Processing
About this paper
Cite this paper
Qian, K., Nymeyer, A., Susanto, S. (2005). Abstraction-Guided Model Checking Using Symbolic IDA* and Heuristic Synthesis. In: Wang, F. (eds) Formal Techniques for Networked and Distributed Systems - FORTE 2005. FORTE 2005. Lecture Notes in Computer Science, vol 3731. Springer, Berlin, Heidelberg. https://doi.org/10.1007/11562436_21
Download citation
DOI: https://doi.org/10.1007/11562436_21
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-29189-3
Online ISBN: 978-3-540-32084-5
eBook Packages: Computer ScienceComputer Science (R0)