Formal verification is becoming a fundamental step of safety-critical and model-based software development. As part of the verification process, model checking is one of the current advanced techniques to analyse the behaviour of a system. Symbolic model checking is an efficient approach to handling even complex models with huge state spaces. Saturation is a symbolic algorithm with a special iteration strategy, which is efficient for asynchronous models. Recent advances have resulted in many new kinds of saturation-based algorithms for state space generation and bounded state space generation and also for structural model checking. In this paper, we examine how the combination of two advanced model checking algorithms – bounded saturation and saturation-based structural model checking – can be used to verify systems. Our work is the first attempt to combine these approaches, and this way we are able to handle and examine complex or even infinite state systems. Our measurements show that we can exploit the efficiency of saturation in bounded model checking.
1. Biere, A., Cimatti, A., Clarke, E. M., and Zhu, Y. Symbolic model checking without BDDs. In Proceedings of the 5th International Conference on Tools and Algorithms for Construction and Analysis of Systems, TACAS’99. Springer-Verlag, London, UK, 1999, 193–207.
2. Bradley, A. R. SAT-based model checking without unrolling. In VMCAI’11. Springer-Verlag, Berlin, Heidelberg, 2011, 70–87.
3. Bruns, G. and Godefroid, P. Model checking partial state spaces with 3-valued temporal logics. In CAV’99. Springer-Verlag, London, UK, 1999, 274–287.
4. Buchholz, P., Ciardo, G., Donatelli, S., and Kemper, P. Complexity of memory-efficient Kronecker operations with applications to the solution of Markov models. INFORMS J. Comput., 2000, 12, 203–222.
http://dx.doi.org/10.1287/ijoc.12.3.203.12634
5. Ciardo, G., Lüttgen, G., and Siminiceanu, R. Saturation: an efficient iteration strategy for symbolic state space generation. In Proc. Tools and Algorithms for the Construction and Analysis of Systems (TACAS). LNCS 2031. Springer-Verlag, 2001, 328–342.
http://dx.doi.org/10.1007/3-540-45319-9_23
6. Ciardo, G., Marmorstein, R., and Siminiceanu, R. The saturation algorithm for symbolic state-space exploration. Int. J. Softw. Tools Technol. Transf., 2006, 8(1), 4–25.
http://dx.doi.org/10.1007/s10009-005-0188-7
7. Ciardo, G. and Miner, A. S. Storage alternatives for large structured state spaces. In Proceedings of the 9th ICCPE: Modelling Techniques and Tools. Springer-Verlag, London, UK, 1997, 44–57.
8. Ciardo, G. and Siminiceanu, R. Structural symbolic CTL model checking of asynchronous systems. In Computer Aided Verification (CAV’03). LNCS 2725. Springer-Verlag, 2003, 40–53.
9. Clarke, E., Grumberg, O., and Peled, D. A. Model Checking. The MIT Press, 1999.
10. Clarke, E., McMillan, K., Campos, S., and Hartonas-Garmhausen, V. Symbolic model checking. In Computer Aided Verification (Alur, R. and Henzinger, T., eds). Lecture Notes in Computer Science, Vol. 102. Springer, Berlin, Heidelberg, 1996, 419–422.
http://dx.doi.org/10.1007/3-540-61474-5_93
11. Heljanko, K. Bounded reachability checking with process semantics. In Proceedings of the 12th International Conference on Concurrency Theory, CONCUR ’01. Springer-Verlag, London, UK, 2001, 218–232.
12. Kleene, S. Introduction to Metamathematics. Bibliotheca mathematica. Wolters-Noordhoff Pub., 1971.
13. McMillan, K. L. Interpolation and SAT-based model checking. In CAV, 2003, 1–13.
14. Ogata, S., Tsuchiya, T., and Kikuno, T. SAT-based verification of safe Petri nets. In ATVA’04. LNCS 299. Springer, 2004, 79–92.
15. Saad, R., Dal Zilio, S., and Berthomieu, B. Mixed shared-distributed hash tables approaches for parallel state space construction. In 10th International Symposium on Parallel and Distributed Computing (ISPDC~2011), Cluj-Napoca, Romania, July 2011. IEEE Computer Society. 2011, 9–16.
16. Schuele, T. and Schneider, K. Three-valued logic in bounded model checking. In MEMOCODE’05. IEEE Computer Society, Washington, DC, USA, 2005, 177–186.
17. Skolem, T. A set theory based on a certain 3-valued logic. Mathematica Scandinavica, 1960, 8, 127–136.
18. Vörös, A., Bartha, T., Darvas, D., Szabó, T., Jámbor, A., and Horváth, Á. Parallel saturation based model checking. In 10th International Symposium on Parallel and Distributed Computing (ISPDC 2011), Cluj-Napoca, July 2011}. IEEE Computer Society, 2011, 94–101.
19. Yu, A., Ciardo, G., and Lüttgen, G. Decision-diagram-based techniques for bounded reachability checking of asynchronous systems. Int. J. Softw. Tools Technol. Transf., 2009, 11, 117–131.
http://dx.doi.org/10.1007/s10009-009-0099-0
