Course Contents

1. Introduction

   • System Verification

   • Definition of Model Checking

   • Model Checking versus Theorem Proving, Debugging

2. System Modelling with Automata

   • Introductory Examples

   • Automata: Definitions

   • Synchronized Products

   • Synchronization by Message Passing and Shared Variables

   • Automata Model for Peterson's Algorithm

3. System Properties Specification with Temporal Logics

   • The Language of Temporal Logic

   • The Formal Syntax of Temporal Logic

   • The Semantic of Temporal Logic

   • PLTL and CTL

   • The Proof System for PLTL

   • The Expressiveness of CTL*

4. Model Checking Algorithms

   • Model Checking CTL

   • Model Checking PLTL

   • The State Explosion Problem

5. Symbolic Model Checking

   • What is symbolic model checking

   • Symbolic Computation of State Sets

   • Symbolic Representation of Sets

   • Binary Decision Diagrams (BDD)

   • Representing Automata by BDDs

   • BDD-based Modelchecking

6. Abstraction Methods

   • Why is Model Abstraction Required

   • Abstraction by State Merging

   • What Can Be Proved in the Abstract Automaton

   • Abstraction on the Variables

   • Abstraction by Restriction

   • Observer Automata

7. SPIN Model Checker

   • What Can We Do with SPIN

   • SPIN's Essentials

   • PROMELA Language

   • Describing Processes with PROMELA

   • Simulating the System

   • Verification of Assertions

   • Verification of PLTL formulas

   • Case Studies

   • Documentation