Things to do

CS 5383 Fall 2007

Topics in Software Development: Model Checking

Software systems are correct if they meet their design requirements. While a few tests may show that a program can meet its requirements, we need to demonstrate that a system cannot fail to meet its requirements. Consider for example the situation where process scheduling decisions are made simultaneously by different processors at distinct locations in a network. The non-determinism of concurrent system executions makes it impossible to devise a traditional test suite with sufficient coverage. Concurrent programs abound: web applications, web services, multi-processor algorithms, telecommunications, even simple Java code that utilizes threads execute with concurrent behavior.

One approach to checking the correctness of software designs is called model checking. We can build a simplified model of the underlying design that preserves its essential characteristics, but avoids the sources of complexity. This model can be verified. In 2002, the SPIN model checker, developed at AT&T Bell Labs, was recognized by the ACM with the Software System Award, placing it with ground breaking software such as UNIX, TCP/IP, Postscript, and TeX.

CS5383 Topics in Software Development: Model Checking will focus on the theory and use of the SPIN model checker for verification of concurrent software. I will assume that you know how to program in some third-generation programming language such as Java, C#, or C. I will also assume that you understand how to construct test cases and test suites. I will refer to concurrent programs and draw on examples from operating systems.

By the end of the course you will be able to:

Recognize the difficulty in adequately testing concurrent programs;
Be able to identify concurrency in programs;
Be able to create a model in Promela, the language of SPIN, that accurately reflects the nature of a program;
Be able to formally specify properties of the system in temporal logics such as LTL and CTL;
Be able to understand specifications of properties written in temporal logics such as LTL and CTL;
Be able to use SPIN to verify concurrent programs;
And Be able to explain how SPIN verifies programs.

Syllabus

Assignments (updated 11/27/07)

LTL Equivalences (updated 10/22/07)

Writing Assessment (updated 9/25/07)

Holzmann lecture for 10/25/07 (updated 10/24/07)

Holzmann lecture for 11/01/07 (updated 10/24/07)

Holzmann lecture for 11/06/07 (updated 10/30/07)

Holzmann lecture for 11/08/07 (updated 10/30/07)

Holzmann lecture for 11/13/07 (updated 10/30/07)

Holzmann lecture for 11/15/07 (updated 10/30/07)

Peer Review Evaluation Rubric (updated 10/30/07)

NASA Practitioner's Handbook (New to this site 11/21/07)