Verification using Model Checking

VU 3   SS 2007   LVA 703800

Description

Prerequisites

• Logic or Logic in Computer Science
  (For dealing with the temporal logics.)
• Semantics of Programming Languages
  (For the semantics of process algebras.)

Topics (not in lecturing order)

Property Specification.

• Syntax and semantics of LTL, CTL, CTL*, modal mu-calculus
• Hierarchy of LTL, CTL, CTL*, modal mu-calculus
• Translation between informal descriptions and formula's
• safety, liveness, fairness

Model Specification

• automata based
  • timed automata
  • annotated finite automata
  • basics of state charts (briefly)
• process algebra based
  • basics: actions, sequential compostion, choice
  • intermediate: parallel composition and recursive equations
  • advanced: synchronisation (LOTOS style, pi-calculus style, (maybe ABP style))
  • adding in (abstract) data types

Algorithms

• automata theoretic approach to LTL
  • LTL to Buechi transformation
  • Nested depth first search
  • Transforming a Buechi Automaton for fairness
• encoding into boolean vector, BDD, SAT.

Miscellaneous

• introduction and overview
• message sequence charts