IEEE Kitchener - Waterloo Section Home Page

University of Waterloo
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 space.

Date:                Thursday 14 August 2003
Location:                University of Waterloo, Davis Centre Room 1304
Time:             9:00 a.m. to 4:00 p.m.
Instructor:       Prof. Dr. Stefan Leue

Institute for Computer Science

Albert-Ludwigs-University

Freiburg, Germany

Overview
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 code.

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

The course 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 customers.

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.

Program

9:00     An Introduction to Model Checking of Software, morning session
Prof. Dr. Stefan Leue, Institute for Computer Science
   Albert-Ludwigs-University Freiburg, Germany
     (http://tele.informatik.uni-freiburg.de/leue)

12:00      Lunch (provided with registration fee)

1:00      An Introduction to Model Checking of Software, afternoon session

4:00    End

Registration Information
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

REGISTRATION FORM

TO REGISTER
Email/Fax/Phone: Vera Korody, Institute for Computer Research, University of Waterloo, Phone: 519-888-4530, Fax: 519-746-5036, Email: vkorody@uwaterloo.ca. Note: registrants paying by credit card please fax your completed registration form and include an authorization signature.

Name:

Position:

Company:

Address:

Address:

City:

Province:

Postal Code:

Telephone:

Fax:

Email:

FEE
$200.00 per registrant + GST = $214.00

        (GST # R119260685)
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. Supervisor:

_____ Other

PAYMENT METHOD

____ Cheque enclosed. Amount: $         (payable to University of Waterloo)

_____ Charge to: ____ Visa   ____ MasterCard

Card #

Expiry Date:

Name on the Card:

Amount: $

Authorization Signature:

____ UW Account Number:

CANCELLATION POLICY
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.