Advanced Tutorial at ACSD 2006 / Petri Nets 2006

Bounded Model Checking

Keijo Heljanko and Tommi Junttila

Turku, Finland, June 26, 2006

Introduction

Model checking [1] is a set of methods for analysing whether a model of a system (e.g., a Petri net) fulfils its specification given as a temporal logic formula. Bounded model checking (BMC) [2] was introduced to further improve the scalability of model checking by applying methods based on propositional satisfiability (SAT). In bounded model checking only counterexample executions of the system that are shorter than some fixed length are considered. The success of BMC, especially in the context of hardware verification, is based on the enormous advances in SAT solving techniques achieved during the last few years.

Contents

The aim is to introduce both basic and advanced bounded model checking topics in a way accessible to both Petri Nets 2006 and ACSD 2006 conference attendees. The main focus is on topics which arise when creating an efficient bounded linear temporal logic (LTL) model checker for an asynchronous system model (e.g., a 1-safe Petri net). This requires the use of efficient SAT encodings for the model checking problem at hand.

List of topics to covered:

Schedule:

Tutorial material:

The tutorial will assume basic understanding of Place/Transition nets and their behaviour. Also basic knowledge of propositional logic is needed. Apart from these prerequisites the tutorial will be self-contained. The tutorial will be based on material published in [3-8].

Tutorial Organizers

Keijo Heljanko
Helsinki University of Technology (TKK)
Laboratory for Theoretical Computer Science
P.O. Box 5400
FI-02015 TKK
Finland
Tommi Junttila
Helsinki University of Technology (TKK)
Laboratory for Theoretical Computer Science
P.O. Box 5400
FI-02015 TKK
Finland

Links

ACSD 2006 / Petri nets 2006 homepage

References

  1. Clarke, E. M., Grumberg, O., and Peled, D. A.: Model Checking, MIT press, 2000.
  2. Biere, A., Cimatti, A., Clarke, E. and Zhu, Y.: Symbolic Model Checking without BDDs. In Proceedings of the 5th International Conference on Tools and Algorithms for the Analysis and Construction of Systems (TACAS'99), pages 193-207, Lecture notes in Computer Science 1579, Springer-Verlag, 1999.
  3. Keijo Heljanko. Bounded reachability checking with process semantics. In Kim Guldstrand Larsen and Mogens Nielsen, editors, Proceedings of the 12th International Conference on Concurrency Theory (Concur' 2001), volume 2154 of Lecture Notes in Computer Science, pages 218-232, Aalborg, Denmark, August 2001. Springer-Verlag.
  4. Keijo Heljanko, Tommi Junttila, and Timo Latvala. Incremental and complete bounded model checking for full PLTL. In Proceedings of the 17th International Conference on Computer Aided Verification (CAV'2005), Lecture Notes in Computer Science 3576, pages 98-111, Edinburgh, Scotland, United Kingdom, to appear. Springer-Verlag.
  5. Keijo Heljanko and Ilkka Niemelš. Bounded LTL model checking with stable models. Theory and Practice of Logic Programming, 3(4&5): 519-550, 2003.
  6. Toni Jussila, Keijo Heljanko, and Ilkka Niemelš. BMC via on-the-fly determinization. STTT - International Journal on Software Tools for Technology Transfer, 7(2):89-101, 2005.
  7. Timo Latvala, Armin Biere, Keijo Heljanko, and Tommi Junttila. Simple bounded LTL model checking. In Alan Hu and Andy Martin, editors, Proceedings of the 5th International Conference on Formal Methods in Computer-Aided Design (FMCAD'04), volume 3312 of Lecture Notes in Computer Science, pages 186-200. Springer-Verlag, November 2004.
  8. Timo Latvala, Armin Biere, Keijo Heljanko, and Tommi Junttila. Simple is better: Efficient bounded model checking for past LTL. In Radia Cousot, editor, Proceedings of the 6th International Conference on Verification, Model Checking and Abstract Interpretation (VMCAI'2005), volume 3385 of Lecture Notes in Computer Science, pages 380-395, Paris, France, January 2005. Springer-Verlag.

Last modified: Fri Mon 19 2005