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.

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:

Bounded Model Checking Basics
Encoding a Transition Relation - Exploiting Concurrency
Combining Partial Order Methods with LTL Model Checking
Encoding LTL Properties
Incremental Bounded Model Checking
Making Bounded LTL Model Checking Complete
Encoding PLTL Properties

Schedule:

9:00 - 10:30 Tutorial part 1 - Keijo Heljanko: BMC basics
10:30 - 11:00 Coffee break
11:00 - 12:30 Tutorial part 2 - Keijo Heljanko: Exploiting concurrency in BMC
12:30 - 13:30 Lunch
13:30 - 15:00 Tutorial part 3 - Tommi Junttila: Encoding LTL in BMC
15:00 - 15:30 Coffee break
15:30 - 17:00 Tutorial part 4 - Tommi Junttila: Incremental and complete BMC, PLTL

Tutorial material:

Slides for tutorial parts 1-2 as PDF, as gzipped Postscript, 4 slides per page.
Slides for tutorial parts 3-4 as PDF, as gzipped Postscript, 4 slides per page.
Demo for tutorial parts 1-2 as PDF, as gzipped Postscript, 4 slides per page.
Nets, circuits, and tools used in the demo for parts 1-2: README-demo.txt, Demo nets, circuits, and BMC tools (18 Megabytes).

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

Clarke, E. M., Grumberg, O., and Peled, D. A.: Model Checking, MIT press, 2000.
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.
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.
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.
Keijo Heljanko and Ilkka Niemelä. Bounded LTL model checking with stable models. Theory and Practice of Logic Programming, 3(4&5): 519-550, 2003.
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.
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.
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