X
X
X

X
Swayam Central

Model Checking

By Prof. Srivathsan.B   |   Chennai Matematical Institute
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.  

INTENDED 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.
PREREQUISITES : Familiarity with basic algorithms and finite-state machines preferable
INDUSTRY SUPPORT : NIL

Learners enrolled: 110

SUMMARY

Course Status : Upcoming
Course Type : Elective
Duration : 12 weeks
Start Date : 27 Jan 2020
End Date : 17 Apr 2020
Exam Date : 25 Apr 2020
Enrollment Ends : 03 Feb 2020
Category :
  • Computer Science and Engineering
  • Level : Undergraduate
    This is an AICTE approved FDP course

    COURSE LAYOUT

    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: Binary Decision Diagrams (BDDs)
    Week 12: Models with timing constraints – timed automata Regular properties – automata over finite words

    BOOKS AND REFERENCES

    Principles of Model-checking, Christel Baier and Joost-Pieter Katoen, MIT Press (2008)

    INSTRUCTOR BIO

    Prof. Srivathsan.B

    Chennai Matematical Institute
    B. Srivathsan obtained his B. Tech and M. Tech (CSE) from IIT Bombay; and Ph.D from the University of Bordeaux, France. He worked as a post-doctoral researcher at RWTH university - Aachen, Germany. He has been a faculty member at CMI since 2013. His main research interest is in the formal verification of real-time systems. 

    COURSE CERTIFICATE

    • The course is free to enroll and learn from. But if you want a certificate, you have to register and write the proctored exam conducted by us in person at any of the designated exam centres.
    • The exam is optional for a fee of Rs 1000/- (Rupees one thousand only).
    • Date and Time of Exams: 25th April 2020, Morning session 9am to 12 noon; Afternoon Session 2pm to 5pm.
    • Registration url: Announcements will be made when the registration form is open for registrations.
    • The online registration form has to be filled and the certification exam fee needs to be paid. More details will be made available when the exam registration form is published. If there are any changes, it will be mentioned then.
    • Please check the form for more details on the cities where the exams will be held, the conditions you agree to when you fill the form etc.

    CRITERIA TO GET A CERTIFICATE:
    • Average assignment score = 25% of average of best 8 assignments out of the total 12 assignments
     given in the course. 
    • Exam score = 75% of the proctored certification exam score out of 100
    • Final score = Average assignment score + Exam score

    YOU WILL BE ELIGIBLE FOR A CERTIFICATE ONLY IF AVERAGE ASSIGNMENT SCORE >=10/25 AND EXAM SCORE >= 30/75. 
    • If one of the 2 criteria is not met, you will not get the certificate even if the Final score >= 40/100.
    • Certificate will have your name, photograph and the score in the final exam with the breakup.It will have the logos of NPTEL and IIT Madras. It will be e-verifiable at nptel.ac.in/noc.
    • Only the e-certificate will be made available. Hard copies will not be dispatched.

    DOWNLOAD APP

    FOLLOW US