Advanced Topics in Software Systems (Formal
Methods for Reactive Systems)
Main Textbook:
Alur R.
and Henzinger T.A., “Computer Aided Verification,”
Draft, 1999.
Other Textbooks:
Manna Z. and Pnueli A., “The Temporal Logic
of Reactive and
Concurrent Systems: Specification,” Springer-Verlag
New York, Inc.,
1992.
Clarke E.M., Grumberg O., and Peled D.A., “Model Checking,” MIT Press, 1999.
Topics:
The course introduces the
theory and practice of formal methods for the design and analysis of concurrent
and reactive systems. The emphasis is on the underlying logical and
automata-theoretic concepts, the algorithmic solutions, and heuristics to cope
with the high computational complexity. Topics include
- Models and semantics of
reactive systems: states vs. events, non-determinism vs. concurrency,
synchrony vs. asynchrony, safety vs. live-ness, refinement preorders,
real-time and hybrid systems, open systems.
- Verification algorithms:
temporal logic model checking, theory of omega automata, serializability and control, minimization.
- Verification techniques: symbolic
model checking, on-the-fly model checking, state space reduction methods,
compositional and hierarchical reasoning, abstract interpretation.
Syllabus
- Computer-Aided
Verification (Introduction)
- Formal Verification
- Automated Verification
- Reactive Systems
- Requirements
- Model Checking
- Hierarchical
Verification
- Software Verification
- Reactive Modules
- Definition of Reactive
Modules
- Operations on Reactive
Modules
- Parallel Composition
- Variable Renaming
- Variable Hiding
- Examples of Reactive
Modules
- Synchronous Circuits
- Shared Variable
Protocols
- Message-Passing
Protocols
- Asynchronous Circuits
- Invariant Verification
- Transition Graphs
- Definition of
Transition Graphs
- From Reactive Modules
to Transition Graphs
- The Reachability Problem
- Invariants
- The
Invariant-Verification Problem
- From Invariant
Verification to Reachability
- Monitors
- Graph Traversal
- Reachabilty
Checking
- Enumerative Graph and
Region Representations
- Invariant Verification
- Three Space
Optimization
- State Explosion
- Hardness of Invariant
Verification
- Complexity of
Invariant Verification
- Compositional
Reasoning
- Composing Invariants
- Assuming Invariants
- Symbolic Graph
Representation
- Symbolic Invariant
Verification
- Symbolic Search
- Symbolic
Implementation
- Binary Decision
Diagrams
- Ordered Binary
Decision Graphs
- Ordered Binary
Decision Graphs
- Operations on BDDs
- Symbolic Search using
BDDs
- Graph Minimalization
- Graph Partitions
- Reachability-preserving
Partitions
- Graph Symmetries
- Partition Refinement
- The Structure of
Stable Partitions
- Partition-refinement
Algorithms
- Reachable Partition
Refinement
- Temporal Logic
- State Formulas
- Temporal Formulas:
Future Operators
- Temporal Formulas:
Past Operators
- Basic Properties of the
Temporal Operators
- A Proof System
- Axioms for a Proof
System
- Basic Interface Rules
- Derived Interface
Rules
- Equality and
Quantifiers
- From General Validity
to Program Validity
- Temporal Safety
Requirements
- Logical Requirements
of Reactive Modules
- Observation
Structures
- State Logics
- Safe Temporal Logic
- Model Checking
- Enumerative Stl Model Checking
- Symbolic Stl Model Checking
- The Distinguishing
Power of Stl
- State Equivalences
- Bi-similarity
- Requirement-preserving
Equivalences
- Stutter-intensive
Equivalences
- The Expressive Power
of Stl
- Automata-theoric Safety Verification
- Automata
- Safe Automaton Logic
- Syntax and Semantics
- The Distinguishing
Power of Stl
- Operations on Automata
- Determinization
- Boolean Operations
- Complementation
- Model Checking