Contents
, Schedule
, Examination
, Course Material
, Info on SPIN
Software systems are becoming an important part of the infrastructure
of our society. Correctness and reliability have become issues of outmost
importance. Testing and correction of software systems are irksome
processes which typically consume half of the resources for system
development. Thus, we need tools for
analyzing software systems with the purpose of checking that they
conform to their intended behavior, and for locating imperfections
(``bugs'') that will cause run-time errors, security vulnerabilities,
crashes, undelivered functionality, etc.
This course concentrates on techniques to verify and find bugs in
concurrent and parallel software systems. Problems that arise from the
parallel execution of several threads, processes, or components are
particularly hard to find a diagnose. In particular, the course teaches
model checking. Model checking techniques can automatically analyze
a pseudo-code description of a communication protocol, a concurrent algorithm,
etc. and find all potential errors. The course will also cover basics of
structured testing for concurrent and parallel software, as well verification
of software.
The material will be practically demonstrated with the
tool SPIN. Spin supports a high level language to specify systems descriptions,
called PROMELA (a PROcess MEta LAnguage). Spin has been used to trace logical design errors in distributed systems design, such as operating systems, data communications protocols, switching systems, concurrent algorithms, railway signaling protocols, etc. The tool checks the logical consistency of a specification. It reports on deadlocks, unspecified receptions, flags incompleteness, race conditions, and unwarranted assumptions about the relative speeds of processes.
Spin can also be used to illustrate techniques in structured software testing,
and has an extension to extract verification models from ANSI-C code.
First Session, April 19-20
Background
Contents
The course is conducted in three two-day sessions. The topics covered
at each session are:
The first session will cover modeling, specification, and verification, using
the paradigm of linear-time temporal logic and the
"automata-theoretic approach". It will also cover the SPIN tool and the
Promela language, which are built on these concepts.
Second Session, May 8-9
The second session will cover algorithms that make the verification of
correctness properties efficient. It will show how to optimize models to make
them amenable to verification. Specific classes of protocols, distributed
algorithms, etc. will be presented, modeled, and discussed from the point
of view of verification.
Third Session, May 29-30
The third session will briefly cover extensions of the verification techniques to cover
test generation and verification of software (given in ANSI-C).
For the verification of ANSI-C programs, there is an extension of SPIN,
ModEx, which transforms C programs into Promela to allow formal verification.
The course will use the
SPIN tool.
Preliminary Schedule
Preliminary Schedule April 19:
Preliminary Schedule April 20:
Preliminary Schedule May 8
Preliminary Schedule May 9
Preliminary Schedule May 29
Preliminary Schedule May 20
Examination
The following are part of examination
Homework Assignments
Course Material
Course material covering the different parts of the course:
There are several written accounts of the automata-theoretic approach
to formal verification, with varying degrees of accessibility. examples are
Overnight exercise:
trono1,
trono2,
trono3,
trono4,
Elevator (due to Holzmann).
5 way handshake (full).
5 way handshake (abstraction).
SPIN: some information.
Reference Material
Following are papers and books that are relevant for the course.