Teaching Staff
- Instructor: Juergen Dingel, Goodwin Hall 723, dingel@cs, office hours: Wednesdays, 11-12
- TA: Scott Grant, Goodwin Hall 624, scott@cs, office hours: Thursdays, 4-5pm, in Goodwin 248
Time and place
Monday 8:30-9:30am, Tuesday 10:30-11:30am and Thursday at 9:30-10:30am, Jeffrey Hall, Room 102.
Audience
CISC 853 is an introduction to software model checking, that is,
the automated, functional analysis of software using finite-state
exploration techniques. It is suitable for students with a general
background in computer science or electrical and computer engineering.
General Description
This course is motivated by two trends in modern software
development:
- Increase in complexity of software:
The size of the software we built is ever increasing
(in 1983, Microsoft Word had 27,000 lines of code;
now it has over a million).
In addition, more and more software is built using several
concurrently executing processes or machines that are
distributed over a network.
The complexity of the resulting systems renders
traditional quality assurance techniques such as
inspection and testing insufficient to ensure
reasonable degrees of reliability.
- Increase in reliance on software:
We increasingly rely on computers and the software they run
to keep our society functioning. In addition, the amount of
software in embedded systems such as micro-controllers in
automobiles, aircraft, medical devices, military equipment,
etc is increasingly dramatically.
Most of this software must be extremely reliable. Failures
can result in huge financial costs or even loss of life.
The combination of these two trends means that in the future,
the potential costs of software failure will grow while
the likelihood of failure will increase.
Experts in academia and industry agree that this situation
is worrying and must be addressed by increasing
our ability to control the complexities of the present
and future software systems.
Recent advances in computer-aided verification have made
various kinds of fully automatic formal analyses
of software feasible even in large-scale industrial contexts.
In particular, finite-state verification (FSV) techniques such as
model checking are emerging as viable means to ensure
high-quality of software.
In FSV, systems are modeled as finite-state automata and
the properties they should satisfy are expressed in some
formal notation such as temporal logic. The analysis of
the system then proceeds by exhaustively exploring the
state space of the system and checking that the property
is met in every state. Although this technique is
exponential in the worst case, it is now used in
many parts of industry (e.g., INTEL, Motorola, Siemens,
Bell Labs, IBM, NASA, Cadence, and Microsoft)
and has helped to validate crucial properties of, e.g.,
on-board spacecraft controllers, network protocols,
graphical user interfaces, railway interlocking systems,
and industrial control systems.
The goals of this course are to
- present the fundamental concepts, techniques,
and research challenges of software model checking
- give students an in-depth understanding of existing software
model checking tools. In particular,
the Bogor software model checker developed at
Kansas State University and
the Spin model checker developed at Bell Labs will be
presented in detail, but other software model
checkers such as VeriSoft (Bell Labs), JPF2 (NASA Ames),
SLAM (Microsoft), and Blast (UC Berkeley) will also be
discussed
- give students some practical experience with the use,
advantages and disadvantages of existing software model checkers
- introduce students to the research in the field.
The course balances theoretical and practical elements
and is most suitable for graduate students
interested in the theory and practice of software development in
general and of software analysis in particular.
Material
- Text book:
Gerard Holzmann. The Spin Model Checker: Primer and Reference Manual.
Addison Wesley. 2004.
Purchase of the book is recommended, but not required.
- Slides: The lecture slides will be made available.
- On-line material: Most of the tools discussed in the course
have extensive publically accessible web pages.
- Some course notes will be provided by the
instructor.
Prerequisites
Mathematical maturity on the level of CISC 203 and 204
and programming experience (preferably in Java).
Some knowledge of concurrent programming.
Evaluation
- For undergraduate students:
- 4 assignments (60%)
- groups of 1-2 students, 15% each
- Final exam (40%)
- For graduate students:
- 4 assignments (50%)
- groups of 1-2 students, 15% each
- Final exam (20%)
- Project (30%)
- groups of 1-2 students
- proposal, presentation, summary
