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%

DATES

Lecture  Summary 

Readings      

Resources
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
http://www.wisdom.weizmann.ac.il/~harel/SCANNED.PAPERS/OOStatecharts.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.


 

READING:
http://www.kenmcmil.com/smv.html

http://www.cs.cmu.edu/~modelcheck/smv.html

 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