Abstract
This paper introduces a technique for localizing model checking of concurrent state-based systems. The technique, called partial model checking, is fully automatic and performs model checking by gradually specializing the specification with respect to the concurrent components one by one, computing a “concurrent weakest precondition.” Specifications are invariance properties and the concurrent components axe sets of transitions. Both are expressed as predicates represented by Reduced Ordered Binary Decision Diagrams (ROBDDs). The self-reducing properties of ROBDDs are important for the success of the technique.
We describe experimental results obtained on four different examples.
Work supported by the Danish Technical Research Council, project CoDesign.
Chapter PDF
Keywords
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.
References
Henrik R. Andersen. Partial model checking (extended abstract). In Proceedings, Tenth Annual IEEE Symposium on Logic in Computer Science, pages 398–407, La Jolla, San Diego, 26–29 July 1995. IEEE Computer Society Press.
R.E. Bryant. Graph-based algorithms for Boolean function manipulation. IEEE Transactions on Computers, 8(C-35):677–691, 1986.
J. R. Burch, E. M. Clarke, and D. E. Long. Symbolic model checking with partitioned transition relations. In A. Halaas and P. B. Denyer, editors, Proc. 1991 Int. Conf. on VLSI, August 1991.
J. R. Burch, E. M. Clarke, K. L. McMillan, D. L. Dill, and L. J. Hwang. Symbolic model checking: 1020 states and beyond. In Proceedings, Fifth Annual IEEE Symposium on Logic in Computer Science, pages 428–439. IEEE Computer Society Press, 1990.
E.M. Clarke, D.E. Long, and K.L. McMillan. Compositional model checking. In Proceedings, Fourth Annual Symposium on Logic in Computer Science, pages 353–362, Asilomar Conference Center, Pacific Grove, California, June 5–8 1989. IEEE Computer Society Press.
Olivier Coudert, Christian Berthet, and Jean Christophe Madre. Verification of synchronous sequential machines based on symbolic execution. In J. Sifakis, editor, Automatic Verification Methods for Finite State Systems. Proceedings, volume 407 of LNCS, pages 365–373. Springer-Verlag, 1989.
Mads Dam. Compositional proof systems for model checking infinite state systems. In I. Lee and S. Smolka, editors, CONCUR'95, 6th International Conference, volume 962 of Lecture Notes in Computer Science, pages 12–26, Philadelphia, PA, USA, August 21–24 1995.
E.W. Dijkstra. A discipline of programming. Englewood Cliffs, N.J.: Prentice-Hall, 1976.
Jo C. Ebergen and Ad M. G. Peeters. Design and analysis of delay-insensitive modulo-N counters. Formal Methods in Systems Design, 3(3), December 1993.
Patrice Godefroid and Pierre Wolper. A partial approach to model checking. In Proceedings, Sixth Annual IEEE Symposium on Logic in Computer Science, pages 406–415, Amsterdam, The Netherlands, 15–18 July 1991. IEEE Computer Society Press.
R.P. Kurshan and Ken McMillan. A structural induction theorem for processes. In Eighth Annual ACM Symposium on Principles of Distributed Computing, pages 239–248. ACM, 1989.
K.L. McMillan. Symbolic Model Checking. Kluwer Academic Publishers, Norwell Massachusetts, 1993.
Robin Milner. Communication and Concurrency. Prentice Hall, 1989.
Christian D. Nielsen. Performance Aspects of Delay-Insensitive Design. PhD thesis, Department of Computer Science, Technical University of Denmark, 1994.
Jørgen Staunstrup. A formal approach to hardware design. Kluwer Academic Publishers, 1994.
Colin Stirling. A complete compositional modal proof system for a subset of CCS. volume 194 of Lecture Notes in Computer Science, pages 475–486. Springer-Verlag, 1985.
A. Tarski. A lattice-theoretical fixpoint theorem and its applications. Pacific Journal of Mathematics, 5:285–309, 1955.
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 1997 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Andersen, H.R., Staunstrup, J., Maretti, N. (1997). Partial model checking with ROBDDs. In: Brinksma, E. (eds) Tools and Algorithms for the Construction and Analysis of Systems. TACAS 1997. Lecture Notes in Computer Science, vol 1217. Springer, Berlin, Heidelberg. https://doi.org/10.1007/BFb0035379
Download citation
DOI: https://doi.org/10.1007/BFb0035379
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-62790-6
Online ISBN: 978-3-540-68519-7
eBook Packages: Springer Book Archive