Learning Objectives
In today’s world, many safety-critical systems are automatically controlled by an embedded code (automatic cars, aircrafts, pacemakers, etc). As the size and the number of interacting components increase, the design and verification of these control software becomes increasingly complex and highly error-prone. Model checking is a field of research that addresses this challenge by making use of rigorous mathematical techniques. The key idea is to view control software as extensions of finite-state machines - this is the “model” of the software. Verification of the software translates to “checking” if the model satisfies certain properties. This is done by an algorithmic analysis of the model.
Learning outcome
The goal of this course is to understand the theoretical foundations of model Checking technology and get a hands-on experience with a tool that performs model checking.
Required Background
Familiarity with basic algorithms and finite-state machines
Syllabus
Module 1: Modeling software and hardware as finite state machines (automata): Models for simple control code and hardware circuits as transition systems; properties as formal languages; introduction to NuSMV model-checker
Module 2: Automata theory over finite and infinite words: Review of DFAs, NFAs, closure properties; introduction to Büchi automata, non-deterministic and deterministic Büchi automata, closure properties.
Module 3: Temporal logics for specifying properties: Linear Temporal Logic (LTL), converting LTL to Büchi automata, model-checking LTL on transition systems, Computation Tree Logics (CTL and CTL), expressiveness of LTL, CTL and CTL, model-checking CTL on transition systems
Module 4: Approaches for scaling model-checking to real systems: Binary decision diagrams (BDDs), Satisfiability solving based model-checking algorithms
Module 5: Adding time to automata: Modeling systems with timing constraints; introduction to timed automata
References:
-
Principles of Model-checking, Christel Baier and Joost-Pieter Katoen, MIT Press (2008). ISBN-13: 978-0262026499
-
Decision Procedures, Daniel Kroening and Ofer Strichman, Springer (2ed, 2016) ISBN-13: 978-3662504963
Meta Data
- Proposed in: 2017 July
- Proposing Faculty: Deepak Rajendraprasad for Dr. B. Srivathsan (CMI)
- Department / Centre: Computer Science and Engineering
- Programme: B.Tech
- Proposal Type: New course
- Offerings
- 2017 Aug-Dec by Dr. B. Srivathsan (CMI)
Past Offerings
- Offered in July-Dec, 2018 by B. Srivathsan (CMI)
- Offered in July-Dec, 2017 by B. Srivathsan (CMI)
Course Metadata
| Item | Details |
|---|---|
| Course Title | Model Checking |
| Course Code | CS4803 |
| Course Credits | 3-1-0-4 |
| Course Category | PME/PME* |
| Approved on | Senate of IIT Palakkad |