CS 4271 - Critical Systems and their Verification
(Sem 2, 2009/10)
Brief Description
This module seeks to familiarize the students with the basic
concepts of building reliable embedded systems. Various kinds of validation
methods are studied, ranging from validation of models to validation of actual
system implementations. We also study validation of various criteria
(functionality, performance) for embedded systems. There is focus for formal
verification as well as other methods such as static and dynamic analysis.
Course Outline and Lesson Plan
The following is a tentative outline of the lectures and examinations in the
course.
- Lesson 1: Introduction
- Lesson 2: Model validation - Modeling notations
- Lesson 3: Model validation - Model simulation and
model-based testing
- Lesson 4: Model validation - Model checking
- Lesson 5: Model validation - Model checking tools
- Semester break
- Lesson 6: Midterm Examination
- Lesson 7: Performance validation - Timing analysis
- Lesson 8: Performance validation - Scheduling methods
- Lesson 9: Performance validation - Timing
predictability via system support
- Lesson 10: Software validation - Trace analysis and
Debugging methods
- Lesson 11: Good Friday
- Lesson 12: Software validation - Static
property checking of software
- Lesson 13: Validation of communication behavior.
Full details of the course schedule appears in the IVLE
Lesson Plan.
Materials
Text Book
Embedded Systems and Software Validation
by Abhik Roychoudhury, Morgan Kaufmann Systems-on-Silicon Series.
Lecture Notes
The lecture slides will be
emailed to students in the class.
Assessment
Midterm : 20%
Assignments :
30%
Final :
50%
Programming Assignments
Assignment 1:
Modeling assignment using
Rhapsody - 10%
Assignment 2: Verification assignment using
SPIN
- 10%
Assignment 3: Analysis assignment using
Chronos - 10%
Other Course Information
Module
Coordinator
Abhik Roychoudhury, Office : COM1 #03-20
Lectures Friday 11 AM - 2 PM, COM1 02-12
Consultation Friday
3 PM - 5 PM, otherwise send me email to fix an appointment.
Pre-requisites
CS1104 and (CS1231 or CS1231S)