文档介绍：* The Ebook starts from the next page : Enjoy !
Concepts, Algorithms, and Tools
for
Model Checking
Joost-Pieter Katoen
Lehrstuhl f¨ur Informatik VII
Friedrich-Alexander Universit¨at Erlangen-N¨urnberg
Lecture Notes of the Course
“Mechanised Validation of Parallel Systems”
(course number 10359)
Semester 1998/1999
Dedicated to Ulrich Herzog
on the occasion of his 60th birthday
4
Contents
Contents 4
Prologue 9
1 System Validation 15
Purpose of system validation . . . . . . . . . . . . . . . . . . . . . 15
Simulation . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 21
Testing . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 21
Formal verification . . . . . . . . . . . . . . . . . . . . . . . . . . 23
Model checking . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31
Automated theorem proving . . . . . . . . . . . . . . . . . . . . . 37
Some industrial case studies of model checking . . . . . . . . . . . 41
Selected references . . . . . . . . . . . . . . . . . . . . . . . . . . 42
2 Model Checking Linear Temporal Logic 47
Syntax of PLTL . . . . . . . . . . . . . . . . . . . . . . . . . . . . 49
5
6 CONTENTS
Semantics of PLTL . . . . . . . . . . . . . . . . . . . . . . . . . . 51
Axiomatization . . . . . . . . . . . . . . . . . . . . . . . . . . . . 58
Extensions of PLTL (optional) . . . . . . . . . . . . . . . . . . . . 60
Specifying properties in PLTL . . . . . . . . . . . . . . . . . . . . 62
Labelled B¨uchi automata . . . . . . . . . . . . . . . . . . . . . . . 66
Basic model checking scheme for PLTL . . . . . . . . . . . . . . . 72
From PLTL-formulas to labelled B¨uchi automata . . . . . . . . . . 77
Checking for emptiness . . . . . . . . . . . . . . . . . . . . . . . . 91
Summary of steps in PLTL-model checking . . . . . . . . . . . . . 102
The model checker Spin . . . . . . . . . . . .