Institute for Computer Research
Short Course Series
AN INTRODUCTION TO MODEL CHECKING OF SOFTWARE
Verifying that a piece of software is doing what it is supposed to do
is a multi-faceted, non-trivial problem. I will introduce an automated
software analysis method that is capable of automatically locating
errors in software models by exhaustively exploring their state
Thursday 14 August 2003
University of Waterloo, Davis Centre Room 1304
a.m. to 4:00 p.m.
Dr. Stefan Leue
Institute for Computer Science
In essence, Model Checking addresses the problem of determining
whether a model (which, in our terms, corresponds to a software
system) is satisfying a set of specified properties (for instance, its
requirements specification). In this course I will breathe some
practical meaning into this rather dry definition, and give an
overview of existing model checking techniques and tools.
The development of the foundations of model checking started in the
early 1980s when there was much interest in defining mathematical
semantics for programs in order to prove them correct. Within the past
two decades, model checking has evolved into a mature software
analysis technology. The models to be analyzed are often obtained from
UML models, and there is an increasing trend to extract the models
automatically from the software code. The appeal of model checking is
rooted in two of its strengths:
(1) If the model is of finite size, the model checking run will return
with a definite yes/no answer without requiring user interaction.
(2) When a property violation has been found, the model checker will
return an error trace that explains how the property violating state
of the software was reached, which helps greatly to understand faults
in the software model.
As a consequence, model checkers today are much more used as automated
debugging tools to efficiently find unexpected bugs in software models
rather than to verify that the model is correct. Model checking
complements software testing since it tends to locate the unexpected
bugs in the model, whereas testing reveals anticipated bugs in the
In this course I will first discuss where model checking can be
helpful in the software development process, before introducing the
explicit state model checking technology on which I will focus. This
will include an introduction into how to model systems (in part using
the Promela modeling language), how to represent requirements in
suitable machine-readable notations, and how to use the model checker
SPIN (which processes Promela models) in order to analyze system
models. I shall then give a brief overview of the symbolic model
checking approach as implemented in the tool SMV, and briefly describe
real-time model checking as implemented in the UPPAAL model checker. I
will conclude with a description of some industrial applications of
model checking, and unconventional applications of model checking in
test case generation and planning. Extensive hints for further
reading will be offered, including three textbooks.
The course has the character of an hors d'oeuvre to model checking,
enabling the attendee to venture off into the world of model checking
tools in order to solve her or his own problems as an entree.
Who Should Attend
addresses all those who are involved in ensuring the quality of highly
complex software systems: software architects and designers, software
developers, quality assurance engineers, project managers and
This short course is sponsored by NCR Canada Limited and the Institute
for Computer Research, University of Waterloo.
Prof. Dr. Stefan Leue
Stefan Leue is a world-renowned software engineer with over 15 years
of experience in collaborating with industry on commercial software
systems for telecommunications, enterprise information and insurance,
in Europe and North America. He currently directs the tele
Research Group on Computer Networks and Telecommunications at the
University of Freiburg. He serves on several program committees
and organizing committees for conferences related to model checking
and other aspects of software engineering.
9:00 An Introduction to Model
Checking of Software, morning session
Prof. Dr. Stefan Leue, Institute for Computer
12:00 Lunch (provided
with registration fee)
1:00 An Introduction to
Model Checking of Software, afternoon session
The registration fee is $200.00 (+ GST) which includes a copy of the
presentation material on paper and CD, lunch and refreshment breaks.
The fee is waived for employees of NCR Canada Limited. ICR faculty
members and graduate students supervised by ICR faculty members may
attend at a fee of $25.00. Please register by Monday 11 August 2003.
Register early, as space is limited.
AN INTRODUCTION TO MODEL CHECKING OF SOFTWARE SHORT COURSE
Thursday 14 August 2003
Email/Fax/Phone: Vera Korody, Institute for Computer Research,
University of Waterloo, Phone: 519-888-4530, Fax: 519-746-5036, Email:
email@example.com. Note: registrants paying by credit card please
fax your completed registration form and include an authorization
$200.00 per registrant + GST = $214.00
Course fee includes a copy of the presentation materials on paper and
CD, lunch and refreshment breaks. Please indicate category:
_____ Free-of-charge for NCR Canada Limited
_____ ICR Faculty Member, $25.00 per course day
_____ ICR Graduate Student, $25.00 per course day.
____ Cheque enclosed. Amount:
$ (payable to
University of Waterloo)
_____ Charge to: ____ Visa ____
Name on the Card:
____ UW Account Number:
Cancellations received up to five days before the short course are
refundable, minus a $20 administrative charge. Cancellations
made after that date, or non-attendance, are subject to the full
registration fee. Substitutions may be made at any time.
P.S. Please note that this course is free to ICR Faculty
Members and Grad Students supervised by ICR Faculty Members, subject
to availability of space.