ABOUT THE COURSE
Embedded software control many of the safety-critical systems that we
deal with in everyday life: for instance, modern cars are equipped with
software to automatically change gears; pacemakers come with a software
controller to regulate heart beat; aircrafts have flight control software, and
so on. Typically, these (software) controllers have to make decisions based on
inputs coming from multiple interacting components. As the size and the number
of interacting components increase, the design and verification of controllers
becomes increasingly complex. Model checking is a field of research that addresses this challenge by
making use of mathematical models in the design and verification of
controllers. The main idea is to look at the system as a mathematical model -
commonly used models are extensions of finite-state machines. Design
requirements on the controller then get translated to suitable questions on
these mathematical models.The goal of this course is to understand some of the techniques and
tools used in the process of model-checking.
The lecture videos of this course can also be found here.
TARGET AUDIENCE
This course would be relevant to CSE/EE/ECE/IT students.
It would also cater to engineers in the industry who are looking forward to
rigorous design and testing methods.
PRE-REQUISITES
Familiarity with basic algorithms and finite-state
machines preferable
CERTIFICATION EXAM
The exam is optional. Exams will be on 1 November 2015 and 8 November 2015.
Time: 1pm-4pm
The list of cities where the exam will be conducted will be available in the registration form.
Registration url: Announcements will be made when the registration form is open for registrations, most likely in July 2015.
The online registration form has to be filled and the certification exam fee of Rs 1000, needs to be paid.
CERTIFICATE
Certificate will be given to those who register and write the exam. Certificate will have your name, photograph and the score in the final exam.
It will also have the logos of NPTEL and IIT Madras. It will also be e-verifiable on the nptel.ac.in/noc website.
Week 1: Modeling
systems as Finite-state machines
Week 2: Using the
model-checker NuSMV
Week 3: Linear-time properties
for verification
Week 4: Regular
properties – automata over finite words
Week 5: Omega-regular
properties – automata over infinite words
Week 6: Model
checking omega-regular properties
Week 7: Linear
Temporal Logic (LTL)
Week 8: Algorithms
for LTL
Week 9: Computation
Tree Logic (CTL)
Week 10: Algorithms
for CTL
Week 11: Models with
timing constraints – timed automata
Week 12: More on
timed automata
Week 13:
Probabilistic models I
Week 14:
Probabilistic models II
Week 15:
Probabilistic models III
REFERENCE MATERIALS
Principles
of Model-checking, Christel Baier and Joost-Pieter Katoen, MIT Press
(2008)
© 2014 NPTEL - Privacy & Terms - Honor Code - FAQs -
