Office of Academic Affairs
Indian Institute of Science Education and Research Bhopal
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 algorithmSelected Readings
- Principles of Model Checking, MIT Press, 2008 (First Edition), Joost-Pieter Katoen, Christel Baier.
- Logic in Computer Sciences, Modeling and Reasoning about Systems, Cambridge Press, 2004 (Second Edition), Michael Huth, Mark Ryan
 Previous |
Back to Course List | Next  |