**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)

- - 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

Mark Lawford Last modified: Wed Jun 12 20:15:08 EDT 2002