Specification and Verification of Reactive Systems (CIS 842) Home Page

Specification and Verification of Reactive Systems (CIS 842)
Spring 2004

About this course

Instructor

General Reading

We (Matt, Robby, myself) are attempting to develop a set of written notes for this course. Reading will mostly be based on those notes, and updates to those notes will be made available to you as the course progresses. For additional reading on technical aspects of model-checking, you can consult the following text-book.
  • Model-checking, by Edmund M. Clarke, Jr., Orna Grumberg, and Doron A. Peled.
Finally, if you are interested in thinking deeply about basic issues in programming concurrency as well as reading some fascinating commentary on the history of programming concurrent systems, I highly recommend the following book which is a collection of some of the classic papers on concurrent programming with commentary and historical perspective by Brinch Hansen. This book also has a number of concurrent programming language constructs which could be implemented as Bogor extensions as simple exercises.

In addition, you will be reading several papers that provide different perspectives on software model-checking and other papers that will help you learn how to use tools associated with specification approaches. These papers will be posted as the course progresses.


Daily life

All notices and announcements for the course will be implemented using the Yahoo group below. You must join this Yahoo group to receive emails about the course.


Click to subscribe to cis842

Tool Home Pages

Below are the home pages for the tools that will use in the course. Each of these tools is available for windows, linux or solaris platforms. We will have versions of solaris executable on the K-state CIS machines made available. If you want your own copy just download and install (its pretty easy).

  • Bogor is an extensible software model-checking engine developed at Kansas State.
  • Bandera is a tool set developed at Kansas State for model-checking concurrent Java software
  • Spin is a widely distributed explicit-state model-checker developed at Bell Labs.
  • JPF is an explicit-state model-checker developed at NASA Ames Automated Software Engineering Laboratory that works directly on Java byte-code.

Week by week

Lecture notes (2-up pdf format) will be linked from this page after each lecture is posted.

We reserve the right to adjust this schedule based on the interest that the class shows in different topics.

Week 1: Administration

Reading :
  • none
Lecture: Course Administration
Examples for lectures
   January 2004
 S  M Tu  W Th  F  S
18 19 20 21 22 23 24

Objectives

Week 2: Introduction to Model-Checking

Reading :
  • TBA
Lecture: Course Overview
Lecture: Introduction to Model-checking
  • Syntax and informal semantics of BIR-Lite (PDF)
  • Computation Trees (PDF)
  • Simulating BIR-Lite Systems with Bogor (PDF) 

   January 2004
 S  M Tu  W Th  F  S
25 26 27 28 29 30 31

Objectives

Week 3: Introduction to Model-Checking (continued)

Lecture: Overview of Bogor Architecture
Lecture:
  • Core DFS algorithm (PDF) 

   February 2004
 S  M Tu  W Th  F  S
 1  2  3  4  5  6  7

Objectives

Week 4: Depth-bounded search

Lecture :
  • Depth-bounded Search (PDF) 

   February 2004
 S  M Tu  W Th  F  S
 8  9 10 11 12 13 14

Objectives

Week 5: Examples & Bogor Internals

Lecture :
  • Examples (PDF)
Lecture : 
   February 2004
 S  M Tu  W Th  F  S
15 16 17 18 19 20 21

Objectives

Week 6: State-Space Representations


Lecture :
Lecture : 

   February 2004
 S  M Tu  W Th  F  S
22 23 24 25 26 27 28

Objectives

Week 7: Specifications

Lecture : Specification Basics (PDF) 

   February 2004
 S  M Tu  W Th  F  S
29

   March 2004
 S  M Tu  W Th  F  S
    1  2  3  4  5  6

Week 8: Specifications

Lecture : Sequencing Specifications (PDF)
Lecture : Sequencing Specifications (2) (PDF)
Lecture : Progress Properties (PDF)
Lecture : Temporal Logic (PDF)
Lecture : LTL Model Checking (PDF)
Lecture : Specification Patterns (PDF)

   March 2004
 S  M Tu  W Th  F  S
 7  8  9 10 11 12 13

Week 9:

Lecture :
Lecture : 

   March 2004
 S  M Tu  W Th  F  S
14 15 16 17 18 19 20

Week A: Spring Break

   March 2004
 S  M Tu  W Th  F  S
21 22 23 24 25 26 27

Week 10:


Lecture :
Lecture : 

   March 2004
 S  M Tu  W Th  F  S
28 29 30 31

   April 2004
 S  M Tu  W Th  F  S
             1  2  3

Week 11:

Reading :
Lecture :
Lecture : 

   April 2004
 S  M Tu  W Th  F  S
 4  5  6  7  8  9 10

Week 12:

Lecture :
Lecture : 

   April 2004
 S  M Tu  W Th  F  S
11 12 13 14 15 16 17

Week 13: 

   April 2004
 S  M Tu  W Th  F  S
18 19 20 21 22 23 24

Week 14:

Lecture :
Lecture : 

   April 2004
 S  M Tu  W Th  F  S
25 26 27 28 29 30 

   May 2004
 S  M Tu  W Th  F  S
                   1

Week 15:

Reading :
Lecture :
Lecture : 

   May 2004
 S  M Tu  W Th  F  S
 2  3  4  5  6  7  8

Copyright 2001-2004, John Hatcliff, Matthew Dwyer, and Robby. The syllabus and all lectures for this course are copyrighted materials and may not be used in other course settings outside of Kansas State University in their current form or modified form without the express written permission of one of the copyright holders. During this course, students are prohibited from selling notes to or being paid for taking notes by any person or commercial firm without the express written permission of one of the copyright holders.
Maintained by John Hatcliff
[HOME]