ECEA 5901 Temporal Logic Model Checking
2nd course in the Fundamentals of Model Checking.
Instructor: Hao Zheng
This course introduces the basic concepts of functional verification and model checking, highlighting their importance in modern system designs. It explains different modeling formalisms for representing the behavior of hardware and software, which are either suitable for automated analysis or can represent data-dependent controls that are common in computing system designs. Additionally, it describes system compositions with respect to different communication models.
Prior knowledge needed: ECEA 5900 Introduction to Modeling for Formal Verification
Learning Outcomes
- Understand linear-time interpretation of transition systems.
- Specify safety, liveness and fairness properties for linear-time behavior.
- Understand syntax and semantics of LTL.
- Understand automata-based model checking.
- Understand how to reduce LTL model checking to automata-based model checking.
- Understand and be able to use the SPIN model checker to perform model checking.
- Understand syntax and semantics of CTL.
- Be able to use LTL to specify branch time properties.
- Understand CTL model checking algorithms.
- Understand symbolic encodings of transition systems.
- Understand binary decision diagrams (BDDs) and how they represent switch functions.
- Understand symbolic model checking algorithms.
Syllabus
Duration: 4.5 hours
This module introduces concepts of linear-time interpretation of transition systems, and shows how to specify various types of properties on the linear-time behavior.
Duration: 8 hours
This module introduces linear-time logic (LTL) for specifying linear-time properties and framework for deciding truth of LTL formulas with respect to transition systems.
Duration: 5 hours
This module introduces computation tree logic (CTL) for specifying properties and model checking algorithms for deciding truth of CTL formulas with respect to transition systems.
Duration: 28.5 hours
This module introduces basic concepts of symbolic model checking, how transition systems can be encoded as switch functions, mode checking algorithms based on switch functions, and BDDs as a compact representation of switch functions.
Duration: 24.5 hours
This module provides an opportunity to exercise CTL model checking learned in the previous modules.
- Use skills from modules 3 and 4 to model a distributed algorithm in NuSMV modeling language.
- Use skills from module 3 and 4 to specify the correctness requirements of the distributed algorithm in CTL.
- Use skills from module 4 to use the NuSMV model checker to verify whether the model of the distributed algorithm satisfies the CTL formulas.
Grading
Assignment | Percentage of Grade |
| Linear Time Behavior and Properties Quiz | 6% |
| Safety Properties and Invariants Quiz | 6% |
| Liveness Properties and Fairness Quiz | 6% |
| Linear Time Logic (LTL): Syntax and Semantics Quiz | 6% |
| LTL Model checking Quiz | 6% |
| SPIN model checker Quiz | 6% |
| Computation Tree Logic Quiz | 6% |
| CTL Model Checking Quiz | 6% |
| Counterexamples and Witnesses Quiz | 6% |
| Symbolic Representation of Transition Systems Quiz | 6% |
| Ordered Binary Decision Diagrams Quiz | 6% |
| Symbolic Model Checker NuSMV Quiz | 6% |
| Final Project | 28% |
Letter Grade Rubric
Letter Grade | Minimum Percentage |
| A | 93% |
| A- | 90% |
| B+ | 86% |
| B | 83% |
| B- | 80% |
| C+ | 76% |
| C | 73% |
| C- | 70% |
| D+ | 66% |
| D | 60% |
| F | 0% |