Model checking is a method for formally verifying finite-state concurrent systems.
Specifications about the system are expressed as formulas in temporal logics (e.g. CTL,
LTL), and efficient algorithms are used to traverse the model defined by the system and
check if the specification holds or not. Very large state-spaces can often be traversed in
minutes. The technique has been applied to several complex industrial systems, ranging
from hardware to communication protocols to safety critical plants and procedures. Scope of
the Tutorial
The goal
of the tutorial is to provide a practical, hands-on introduction to Model Checking. The
tutorial will be based on the use of two model checkers:
- NuSMV, a symbolic
model checker specialized on the verification of synchronous systems;
- SPIN, an on-the-fly
model checker specialized on the verification of asynchronous systems.
The
tutorial will include an overview of the theoretical background in model checking, a demo
of the tools, and working sessions where the participants will tackle the proposed model
checking problems. Workstations will be available for the participants to use during the
tutorial. During the working sessions, assistants will be available for the participants
to clarify topics of interest and discuss modeling and verification techniques.
Instructors Alessandro
Cimatti
IRST,
Trento, Italy
Email: cimatti@irst.itc.it
Marco Pistore
IRST,
Trento, Italy
Email: pistore@irst.itc.it
Marco
Roveri
IRST,
Trento and
DSI, Università di Milano
Italy
Email: roveri@irst.itc.it
Attendance
The
workshop will be at an introductory level. The registration fee will be kept to a minimum.
However, the number of participants will be limited, in order to guarantee the
availability of computers during the tutorial. Researchers interested in attending should
send a brief application describing their interest in the tutorial.
Important
Dates
- Application:
May 15
- Notification:
May 31
Organization
Alessandro
Cimatti, ITC-irsrt
Trento, Italy
cimatti@irst.itc.it |
