Embedded Systems, MOSIG 2 (Option PDES), University of Grenoble
The course consists of two parts. The first part is taught by Florence Maraninchi.
Please see the course
homepage for more details. The second part is taught by me.
The second part of the course gives an introduction to a verification
technique called model checking. We will consider the two temporal
logics Computation Tree Logic (CTL) and Linear temporal logic (LTL) to
express desired properties. LTL and CTL are the core of industrial
logics like System Verilog Assertions (SVA) or Property Specification
Language (PSL). Given a system and a desired property of the system
(aka the specification), we will study algorithms that check if the
system satisfies the property.
The second part of the course is structured as follows:
- Wednesday Nov 23 (7): Examples of systems and properties that
can be verified by model checking, translation of (simple subset of)
Verilog to transition graphs, definition of Computation Tree Logic
- Wednesday Nov 30 (8): CTL model checking based on fixpoint
- Wednesday Dec 7 (9): Symbolic Model Checking and Binary Decision Diagrams
- Wednesday Dec 14 (10): CTL model checking with
Fairness, Bisimulation, Simulation Relation, and Linear-Time Logic (LTL)
- Wednesday Jan 4 (11): LTL Model Checking
Slides and Course Material
- Slides for lecture on 23/11/2011:
(1) Introduction, Examples, CTL Syntax and Semantics,
- Material for exercises on 23/11/2011:
How to get started with VIS on ensisun,
You can get VIS for your own computer here.
Kripke structure of mutex.v,
CTL formulas for mutex.v,
Verilog Model of elevator,
CTL Formulas for elevator model
- Slides for lecture on 30/11/2011:
(2) CTL Model Checking
- Material for exercises on 30/11/2011:
- Slides for lecture on 7/12/2011:
(3a) Symbolic Model Checking,
(3b) BDDs (thanks to Daniel Kroening for the
- Material for exercises on 7/12/2011:
miniBDD source code,
- Slides for lecture on 14/12/2011:
(4) Fairness constraints,
(5) Bisimluation, Simulation Relation, and Linear Temporal Logic (LTL)
- Material for exercises on 14/12/2011:
Example on how to using fairness constraints in VIS,
- Slides for lecture on 04/01/2012:
(6) LTL Model Checking
- Material for exercises on 04/01/2012:
GOAL - a tool for manupulating Büchi automata,
Links to Related Topics
- Z. Manna and
A. Pnueli. The Temporal Logic of Reactive and Concurrent Systems: Specification,
- Z. Manna and A. Pnueli. Temporal Verification of Reactive Systems: Safety, 1995.
- E. Clarke, O. Grumberg, and D. Peled, Model Checking, 2000.
- C. Baier and J.-P. Katoen, Principles of Model Checking, 2008.
- B. Bérard, M. Bidoit, A. Finkel, F. Laroussinie, A. Petit,
L. Petrucci and
Ph. Schnoebelen. Model-Checking Techniques and
Tools, Springer, 2001. French version: Ph. Schnoebelen, B. Bérard,
M. Bidoit, F. Laroussinie and A. Petit. Vérification de logiciels :
techniques et outils du model-checking. Vuibert, 1999.
Examples of Industrial Verification Tools