CS 4271 - Critical Systems and their Verification
(2010/11).
This an old offering. For 2011-12 offering, see
IVLE
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 - Modeling notations
- Lesson 4: Model validation - Model-based testing,
Test specifications and Temporal Logics
- Lesson 5: Model validation - Model checking tools
- Lesson 6: Inter-component communication
validation
- Lesson 7: Midterm Examination
- Lesson 8: Performance validation - Why timing is
important
- Lesson 9: Performance validation - Software timing
analysis
- Lesson 10: Performance validation - System level
timing predictability
- Lesson 11: Software validation - Trace analysis and
Debugging methods
- Lesson 12: Software validation - Testing,
symbolic execution
- Lesson 13: Review of Lecture Materials
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 appear in
IVLE.
Assessment
Midterm : 25%
Assignments
: 25%
Final :
50%
Programming Assignments (see
IVLE for details)
Assignment 1:
System Modeling assignment using
Rhapsody - 14%
Assignment 2: Performance Analysis assignment using
Chronos - 11%
Other Course Information
Module
Coordinator
Abhik Roychoudhury, Office : COM2
#03-07
Lectures
Wed 12 noon - 3 PM, COM1 02-12
Consultation Whenever
you want to meet me, send me e-mail by proposing a meeting time.
Pre-requisites
Undergraduate background in computer organization and discrete
mathematics.