CS 4271- Critical Systems and their Verification

     Tentative Lesson Plan for 2011-12 Semester 2   

         The full lesson plan is being maintained in IVLE, and students should check IVLE for regular updates.

       General Information:  Instructor, Teaching Assistant, Textbook.           

           Assessment:  Labs 35%, Midterm 25%, Final Exam 40%


Lecture  Summary 



Week 1  

General introduction of embedded systems and the need for validation

General discussion on the statechart notation will be conducted in the later part of the lecture.

First Lab Posted (using Rhapsody for Statechart modeling):  Description, Tool guide, Tool usage notes


Textbook Chapter 1

The following papers may also be useful http://www.wisdom.weizmann.ac.il/~harel/SCANNED.PAPERS/Statecharts.pdf


 First part of lecture

Second part of lecture

Showing Rhapsody tool to students

Week 2 Model Validation - Discussion of Modeling notations


Chapter 2.3 - 2.5 of textbook Lecture Notes


Week 3, Model validation - Model based testing, test specifications



Chapter 2.6,2.7 of textbook Lecture Notes


Week 4 Model validation -Model checking

Chapter 2.8 of textbook

Lecture Notes (LTL)

Lecture notes (MC)

Week 5 SPIN Model Checker

Lab 1 is due - no extensions

Lab2 (on SPIN) is given out.

Chapter 2 (all)

READING:  http://spinroot.com/spin/whatispin.html  contains a

wealth of pointers on SPIN.

Lecture Notes



Week 6 SMV Model Checker

The modeling language of this checker is in the style of hardware.
Time permitting, a real-life case study using SMV is also discussed.




Lecture Notes


                                                                                                      Recess (19 - 27 Feb)  Lab 2 is due - no extensions
Week 7, Midterm Examination 

Lab 3 (on SMV)  is also given out in this week.


-- Midterm solutions to be posted


Week 8


Performance validation - Worst-case Execution time analysis of embedded software. In this lecture, we introduce the problem of timing analysis and why it is important for embedded system design


Chapter 4.1, 4.2

Lecture Notes


Week 9 Performance validation - WCET analysis methods via Timing Schema and Integer Linear Programming. Some in-class exercises on timing analysis will be discussed towards the end of this lecture. These exercises will be given out in class, and posted in IVLE after the class.

As in past week

Lecture Notes.

Week 10


Performance validation (System level):  We wrap up our discussion on performance validation with discussion on scheduling methods such as Rate monotonic Scheduling (RMS) and Earliest Deadline First (EDF).  System support for time-predictable execution will also be studied.

Lab 3 (on SMV) is due - no extensions.

Lab 4 (timing analysis using Chronos) is given out


Chapter 4.3 - 4.5

Lecture Notes


Week 11  

Software Testing and Debugging - we focus on the age-old practice of software testing and how find the error root-cause when a test case fails (i.e. debugging).

Chapter 5.1 Lecture Notes


Week 12  

Software Testing and Debugging - We conclude our discussions by focusing on directed testing via symbolic execution.

Last year's question paper was also discussed as revision exercise in class, and the solutions are posted.

Chapter 5.1 Lecture Notes


Week 13

Communication Validation:  In this final lecture, we discuss validation of inter-component communication among embedded system components.

Lab 4 (timing analysis using Chronos) is due - no extensions



  Chapter 3 Lecture notes