CS 4271 - Critical Systems and their Verification

Brief Description
Materials
Assessment
Other Course Information

Brief Description

This course will introduce verification techniques for safety critical reactive systems. The specific focus will be on embedded systems. We will concentrate on an automated verification technique called Model Checking. This is founded on state space search and can, in principle, check all possible behaviors of a system. The main components of the course will touch upon: (a) modeling of reactive systems (b) formal verification via Model Checking (c) state space reduction techniques to achieve space/time efficiency and (d) general issues in validation of embedded systems.

Materials

Text Book

Model Checking by Clarke, Grumberg, Peled (Available in Bookstore).

Tutorials/Readings

SMV Tutorial by Ken Mcmillan (the first 2-3 sections are useful for our course).
Verification Tools for Finite-State Concurrent Systems, LNCS 803, June 1993 by Clarke, Grumberg, Long

Lecture Notes

You will be able to access the lecture slides from the IVLE area.

Assessment

Midterm : 25%

Lab assignments: 25%
Final : 50%

Other Course Information

Instructor P. S. Thiagarajan, Office : COM1, #03-32 , thiagu@omp.nus.edu.sg
Lectures Friday 11:00 AM - 2 PM at SR3A, COM1 # 212

Consultation Send e-mail to fix an appointment.

Pre-requisites: CS 1231/1231s : Discrete Mathematics and CS 1104 : Computer Organization