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:
- 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
|