×

Exploiting step semantics for efficient bounded model checking of asynchronous systems. (English) Zbl 1243.68213

Summary: This paper discusses bounded model checking (BMC) for asynchronous systems. Bounded model checking is a technique that employs the power of efficient SAT and SMT solvers for model checking. The main contribution of this paper is the presentation of a simple modeling formalism independent way of translating an asynchronous system into a transition formula for three partial order semantics: the \(\exists\)-step semantics, its generalization, the relaxed \(\exists\)-step semantics, and a novel variant that combines the latter with the idea of process semantics. Step and process semantics have been introduced in earlier works for different low level asynchronous system formalisms to improve the efficiency of BMC. However, this paper is the first one showing how to translate the semantics for any asynchronous system modeling formalism including high-level data manipulation operations while encoding the independence of actions in a dynamic fashion. Thus, the approaches have been extended to cover a larger class of modeling formalisms. The technical approach uses the notion of a coherent encoding of the transition relation, making for a simple and elegant translation of the partial order semantics in question. The presented translations have been implemented and we present extensive empirical results comparing the efficiency of the different translations to each other as well as to an explicit state model checker DiVinE on its own BEEM benchmark suite.

MSC:

68Q60 Specification and verification (program logics, model checking, etc.)
68N30 Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.)
68Q55 Semantics in the theory of computing
PDF BibTeX XML Cite
Full Text: DOI

References:

[1] Jr., E. M. Clarke; Grumberg, O.; Peled, D. A.: Model checking, (1999)
[2] Baier, C.; Katoen, J. -P.: Principles of model checking, (2008) · Zbl 1179.68076
[3] Burch, J. R.; Clarke, E. M.; Mcmillan, K. L.; Dill, D. L.; Hwang, L. J.: Symbolic model checking: 1020 states and beyond, Information and computation 98, No. 2, 142-170 (1992) · Zbl 0753.68066
[4] Biere, A.; Cimatti, A.; Clarke, E. M.; Zhu, Y.: Symbolic model checking without bdds, Lncs 1579, 193-207 (1999)
[5] Marques-Silva, J.; Lynce, I.; Malik, S.: CDCL solvers, , 131-153 (2009)
[6] Barrett, C.; Sebastiani, R.; Seshia, S. A.; Tinelli, C.: Satisfiability modulo theories, , 825-885 (2009)
[7] Biere, A.; Heljanko, K.; Junttila, T.; Latvala, T.; Schuppan, V.: Linear encodings of bounded LTL model checking, Logical methods in computer science 2, No. 5:5, 1-64 (2006) · Zbl 1127.68057
[8] Holzmann, G. J.: The model checker spin, IEEE transactions on software engineering 23, No. 5, 279-295 (1997)
[9] Barnat, J.; Brim, L.; Ročkai, P.: Divine 2.0: high-performance model checking, , 31-32 (2009)
[10] Valmari, A.: The state explosion problem, Lncs 1491, 429-528 (1998)
[11] Best, E.; Devillers, R. R.: Sequential and concurrent behaviour in Petri net theory, Theoretical computer science 55, No. 1, 87-136 (1987) · Zbl 0669.68043
[12] Heljanko, K.: Bounded reachability checking with process semantics, Lncs 2154, 218-232 (2001) · Zbl 1006.68081
[13] Rintanen, J.; Heljanko, K.; Niemelä, I.: Planning as satisfiability: parallel plans and algorithms for plan search, Artificial intelligence 170, No. 12–13, 1031-1080 (2006) · Zbl 1131.68099
[14] Kautz, H. A.; Selman, B.: Pushing the envelope: planning, propositional logic and stochastic search, , 1194-1201 (1996)
[15] Malinowski, J.; Niebert, P.: SAT based bounded model checking with partial order semantics for timed automata, Lecture notes in computer science 6015, 405-419 (2010) · Zbl 1284.68412
[16] Dimopoulos, Y.; Nebel, B.; Koehler, J.: Encoding planning problems in nonmonotonic logic programs, Lncs 1348, 169-181 (1997)
[17] Wehrle, M.; Rintanen, J.: Planning as satisfiability with relaxed \(\exists \)-step plans, Lncs 4830, 244-253 (2007)
[18] Ogata, S.; Tsuchiya, T.; Kikuno, T.: SAT-based verification of safe Petri nets, Lncs 3299, 79-92 (2004) · Zbl 1108.68082
[19] Jussila, T.: BMC via dynamic atomicity analysis, , 197-206 (2004)
[20] Jussila, T.; Heljanko, K.; Niemelä, I.: BMC via on-the-fly determinization, International journal on software tools for technology transfer 7, No. 2, 89-101 (2005) · Zbl 1271.68138
[21] T. Jussila, On bounded model checking of asynchronous systems, Research Report A97, Helsinki University of Technology, Laboratory for Theoretical Computer Science, doctoral dissertation, 2005.
[22] Dubrovin, J.; Junttila, T.; Heljanko, K.: Symbolic step encodings for object based communicating state machines, Lncs 5051, 96-112 (2008)
[23] Wang, C.; Yang, Z.; Kahlon, V.; Gupta, A.: Peephole partial order reduction, Lncs 4963, 382-396 (2008) · Zbl 1134.68421
[24] Kahlon, V.; Wang, C.; Gupta, A.: Monotonic partial order reduction: an optimal symbolic partial order reduction technique, Lncs 5643, 398-413 (2009) · Zbl 1242.68166
[25] Burckhardt, S.; Alur, R.; Martin, M. M. K.: Checkfence: checking consistency of concurrent data types on relaxed memory models, , 12-21 (2007)
[26] Dubrovin, J.: Checking bounded reachability in asynchronous systems by symbolic event tracing, Lncs 5944, 146-162 (2010) · Zbl 1273.68226
[27] Mcmillan, K. L.: Using unfoldings to avoid the state explosion problem in the verification of asynchronous circuits, Lncs 663, 164-177 (1993)
[28] Esparza, J.; Heljanko, K.: Unfoldings – a partial-order approach to model checking, EATCS monographs in theoretical computer science (2008) · Zbl 1153.68035
[29] S. Ranise, C. Tinelli, The SMT-LIB standard: Version 1.2, 2006.
[30] Bultan, T.; Gerber, R.; Pugh, W.: Symbolic model checking of infinite state systems using Presburger arithmetic, Lncs 1254, 400-411 (1997)
[31] Graf, S.; Saïdi, H.: Construction of abstract state graphs with PVS, Lncs 1254, 72-83 (1997)
[32] Kesten, Y.; Maler, O.; Marcus, M.; Pnueli, A.; Shahar, E.: Symbolic model checking with rich assertional languages, Theoretical computer science 256, No. 1–2, 93-112 (2001) · Zbl 0973.68119
[33] Rybina, T.; Voronkov, A.: A logical reconstruction of reachability, Lncs 2890, 222-237 (2003) · Zbl 1254.68153
[34] Abdulla, P. A.; Delzanno, G.; Rezine, A.: Parameterized verification of infinite-state processes with global conditions, Lncs 4590, 145-157 (2007) · Zbl 1135.68461
[35] Bouajjani, A.; Habermehl, P.; Jurski, Y.; Sighireanu, M.: Rewriting systems with data, Lncs 4639, 1-22 (2007) · Zbl 1135.68467
[36] Ghilardi, S.; Nicolini, E.; Ranise, S.; Zucchelli, D.: Towards SMT model checking of array-based systems, Lncs 5195, 67-82 (2008) · Zbl 1165.68406
[37] Pelánek, R.: BEEM: benchmarks for explicit model checkers, Lncs 4595, 263-267 (2007)
[38] Junttila, T.; Dubrovin, J.: Encoding queues in satisfiability modulo theories based bounded model checking, Lncs 5330, 290-304 (2008) · Zbl 1182.68122
[39] SRI International, Yices 2.0 prototype, software, 2009. URL: http://yices.csl.sri.com/download-yices2.shtml.
[40] Brummayer, R.; Biere, A.: Boolector: an efficient SMT solver for bit-vectors and arrays, Lncs 5505, 174-177 (2009)
[41] Eén, N.; Sörensson, N.: Temporal induction by incremental SAT solving, Electronic notes in theoretical computer science 89, No. 4, 543-560 (2003) · Zbl 1271.68215
[42] Younger, D. H.: Minimum feedback arc sets for a directed graph, IEEE transactions on circuit theory 10, No. 2, 238-245 (1963)
[43] Diekert, V.; Métivier, Y.: Partial commutation and traces, Handbook of formal languages 3, 457-534 (1997)
[44] Heljanko, K.; Niemelä, I.: Bounded LTL model checking with stable models, Theory and practice of logic programming 3, No. 4–5, 519-550 (2003) · Zbl 1079.68058
[45] Mcmillan, K. L.: Interpolation and SAT-based model checking, Lncs 2725, 1-13 (2003) · Zbl 1278.68184
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. It attempts to reflect the references listed in the original paper as accurately as possible without claiming the completeness or perfect precision of the matching.