Indian Institute of Science Education and Research Bhopal

Bhopal Bypass Road, Bhauri, Bhopal - 462 066, Madhya Pradesh, India
Electrical Engineering and Computer Science

ECS 302: Introduction to Software Modeling and Verification (4)

Learning Objectives:

The design of software and hardware systems is a nontrivial task and is usually accomplished with some kind of formal modeling and verification to gain confidence on the behavior of system under design. This course introduces the fundamentals of model checking which is an automated verification method guaranteeing that a mathematical model of a system satisfies a formally described property. It can be used to asses both the qualitative and quantitative properties of complex software and hardware systems. The aim of this course is to familiarize students with the mathematical and logical foundations behind model checking, and to give them a flavor of how model checking techniques can be employed to improve the reliability and dependability of complex software/hardware systems.

Course Contents:

Part I: How to model software/hardware systems? – transition systems, programs to transition systems, hardware circuits to transition systems, concurrency and interleaving, communication and handshaking, synchronous parallelism, state space explosion problem, modeling tools

Part2:    What are linear-time (LT) properties? deadlock, trace equivalence, liveness, safety, fairness

Part3:    How to model check linear-time (LT) properties? – finite state automata, automata, on infinite words (Buchi) and omega-regular properties, model checking omega-regular properties (nested depth-first search)

Part4:  How to express LT properties concisely? - syntax and semantics of linear-time temporal logic (LTL), examples of LTL properties, expressive power of LTL, model checking algorithms for LTL, fairness in LTL

Part5:    What are branching time properties? – syntax and semantics of computation-tree logic (CTL), examples of CTL properties, expressive power of CTL, LTL vs CTL, model checking algorithms for CTL. Fairness in in CTL, CTL* and its expressiveness

Part6:  How to reduce the size of models? – Equivalences and pre-orders, property preservation and state space minimization algorithm

Selected Readings

Previous Back to Course List Next