CS 734 - FORMAL METHODS FOR REAL-TIME SYSTEMS : Course Outline

Instructor: Assistant Prof. Mark Lawford

Office: JHE/302C

Email: lawford@mcmaster.ca

This course provides an introduction to formal methods including equivalence verification, model-checking, theorem proving and supervisory control theory. Emphasis will be placed on demonstrating how such methods can be adapted to deal with the design and verification of safety-critical real-time control systems. Students will apply theoretical results to both toy and real-world examples, using SRI's Prototype Verification System (PVS) automated theorem prover and other tools.

Required prerequisite knowledge: Previous courses in discrete mathematics and mathematical logic and/or permission of the instructor.

References: The course homepage at: http://www.cas.mcmaster.ca/~lawford/CS734 contains a complete list of references

Marking scheme:

• Course assignments - 50%
• Final project - 40%
• Class participation - 10%

TENTATIVE SYLLABUS: (may be subject to change at intructor's discretion)

LECTURE 1: INTRODUCTION

• - Safety critical real-time control systems
• - Example applications
• - Example failures
• - Example: safety-critical real-time system problem & discussion of implementation issues
• - What is a formal method?
• - Why should we be interested in formal methods?
• - When should they be used?

LECTURE 2: INTRODUCTION TO PVS

• - Sequent calculus and propositional logic in PVS (updated Jan. 16, 2002)
• - Predicate logic in PVS (updated Jan. 16, 2002)

LECTURE 3: TYPES AND TYPECHECKING IN PVS

• - Dealing with partial functions in logic (Notes updated Feb 1, 2002)
• - Types, Subtypes, dependent types and parametrized types (Notes updated Feb 1, 2002)
• - Use of typing in verification to guarantee control system properties
• - Automatic generation and proof of Type Checking Conditions in PVS

LECTURE 4: STATIC ANALYSIS OF SAFETY CRITICAL IN PVS

• - Functional Verification and the 4-Variable model (slides: pdf or postscript)
• - Parnas-style tables as way of guaranteeing domain coverage and determinism of control system specifications and implementations
• - Analyzing Tabular Specifications using PVS (slides for Power Conditioning example: pdf or postscript)
• - Incorporating tolerance relations: The 8-Variable model (slides from AMAST'2000: pdf or postscript - see also the full paper)
• - limitations of static analysis

LECTURE 5: SPECIFYING TIMING IN PVS (slides Notes updated March 15, 2002)

• - Recursion and proof by induction in PVS
• - Previous work on verification of timing in PVS
• - "Clocks" theory
• - Timing operators "Held For", "Delayed by" and "Periodic with period x"
• - Mathematical formalization of operator definitions in continuous and discrete time settings
• - Using PVS libraries: Don't reinvent the wheel!
• - Application Examples

LECTURES 6 & 7: FIXED POINTS, MU-CALCULUS and EXPLICIT STATE MODEL-CHECKING (slides: pdf or postscript)

• - Underlying models, real-time models, composition and state explosion
• - Kripke structures, labeled transition systems, state-event labeled transition systems
• - Real-time models: timed transition models (Ostroff), timed automata (Alur & Dill)
• - Definition of Mu-calculus
• - Overview of logics LTL, CTL, CTL*, RTL and RTTL
• - Detailed description of selected operators using Mu-calculus

LECTURE 8: BDDs & SYMBOLIC MODEL CHECKING (slides: pdf or postscript)

• - Binary Decision Diagrams
• - Theory & examples
• - Overview of main results on symbolic model-checking
• - Benefits & limitations
• - Modelchecking with PVS and other tools

LECTURES 9-10: SUPERVISORY CONTROL THEORY

• - languages, automata and supervisory control
• - controllablility and controller synthesis
• - supervisory control of Timed Discrete Event Systems

LECTURES 11-12: EQUIVALENCE VERIFICATION, COMPOSITIONALLY CONSISTENT MODEL REDUCTION & MODULAR VERIFICATION

• - Equivalence verification
• - Why string equivalence is not enough for concurrent systems
• - Illustrative examples
• - Compositional Consistency and Control Equivalence Property
• - Quotient systems, homomorphisms and computation of equivalences
• - Algebraic definition of State Event observers and relation to observation equivalence
• - TTM state-event equivalence
• - Introduction to model reduction
• - Strong model reduction
• - Formula-specific vs. general model reduction
• - Stuttering-invariant formulas & weak model reduction
• - Compositional model reduction
• - Compositionally consistent model reduction using state-event observers
• - Modular proof techniques