Abstract
This paper presents a method for taking advantage of the efficiency of symbolic model checking using disjunctive partitions, while keeping the number and the size of the partitions small. We define a restricted form of a Kripke structure, called an or-structure, for which it is possible to generate small disjunctive partitions. By changing the image and pre-image procedures, we keep even smaller partial disjunctive partitions in memory. In addition, we show how to translate a (software) program to an or-structure, in order to enable efficient symbolic model checking of the program using its disjunctive partitions. We build one disjunctive partition for each state variable in the model directly from the conjunctive partition of the same variable and independently of all other partitions. This method can be integrated easily into existing model checkers, without changing their input language, and while still taking advantage of reduction algorithms which prefer conjunctive partitions.
Chapter PDF
Similar content being viewed by others
References
Beer, I., Ben-David, S., Eisner, C., Landver, A.: RuleBase: an industry-oriented formal verification tool. In: Proc. DAC 1996, pp. 655–660 (1996)
Cabodi, G., Camurati, P., Lavagno, L., Quer, S.: Disjunctive partitioning and partial iterative squaring: an effective approach for symbolic traversal of large circuits. In: Proc. DAC 1997, pp. 728–733 (1997)
Cabodi, G., Camurati, P., Quer, S.: Auxiliary variables for extending symbolic traversal techniques to data paths. In: Proc. DAC 1994, pp. 289–293 (1994)
Chan, W., Anderson, R., Beame, P., Notkin, D.: Improving efficiency of symbolic model checking for state-based system requirements. In: Proc. ISSTA 1998 (1998)
Eisner, C.: Model checking the garbage collection mechanism of SMV. In: Stoller, S.D., Visser, W. (eds.) Electronic Notes in Theoretical Computer, vol. 55, Elsevier Science Publishers, Amsterdam (2001)
Eisner, C., Peled, D.: Comparing symbolic and explicit model checking of a software system. In: Bošnački, D., Leue, S. (eds.) SPIN 2002. LNCS, vol. 2318, pp. 230–239. Springer, Heidelberg (2002)
Geist, D., Beer, I.: Efficient model checking by automated ordering of transition relation partitions. In: Dill, D.L. (ed.) CAV 1994. LNCS, vol. 818, pp. 299–310. Springer, Heidelberg (1994)
Burch, J.R., Clarke, E.M., Long, D.E.: Symbolic model checking with partitioned transition relations. In: Halaas, A., Denyer, P.B. (eds.) International Conference on Very Large Scale Integration, pp. 49–58 (1991)
McMillan, K.: Symbolic Model Checking. Kluwer Academic Publishers, Dordrecht (1993)
Solé, M., Pastor, E.: Traversal techniques for concurrent systems. In: Aagaard, M.D., O’Leary, J.W. (eds.) FMCAD 2002. LNCS, vol. 2517, pp. 220–237. Springer, Heidelberg (2002)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2003 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Barner, S., Rabinovitz, I. (2003). Efficient Symbolic Model Checking of Software Using Partial Disjunctive Partitioning. In: Geist, D., Tronci, E. (eds) Correct Hardware Design and Verification Methods. CHARME 2003. Lecture Notes in Computer Science, vol 2860. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-540-39724-3_6
Download citation
DOI: https://doi.org/10.1007/978-3-540-39724-3_6
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-20363-6
Online ISBN: 978-3-540-39724-3
eBook Packages: Springer Book Archive