Verification using Model Checking
VU 3 SS 2007 LVA 703800
Course material
(Work in progress, see schedule)
Slides
These slides are 1 per page, convenient for viewing on a screen.
To print multiple pages per sheet, the print menu of acrobat reader offers
a section Page Handling, where Page Scaling can be set to multiple pages per sheet.
Notes
-
Some tips for uppaal.
-
Collected online help in
Open Office and
PDF
-
A very short note on process algebra and
an overview of the transitions rules and axioms.
Homework (graded)
modeling and verification of a traffic light installation
Description in PDF.
modeling and verification of a traffic light installation
-
Description in PDF
-
Deadline 26.4.2007
verification of an elevator (Deadline 11.7.2007)
Given are a model of an elevator
and the first two formulas. The
task is to write a full set of formula's.
- Make sure you cover all of the area's:
- Safety
- Liveness
- Use cases: formula's that show that expected behaviour is present.
(A system that has no behaviour at all trivially satisfies safety
formulas and liveness properties of the form if A then eventually B.)
- Correctness issues: timing requirements, status indicators working as
advertised, etc.
- If a property can only be verified by writing a monitoring process.
Then write one.
- Enough is enough: if a certain category of formula's
leads to tens of formula's, give a few examples and
then write how to do the rest in a comment.
modeling and partial verification of a simplified I2C protocol (Deadline 11.7.2007)
- See the information on the slides and this description
- The model of a wire.
- A web search will yield many source for information about the I2C bus.
E.g. this one.
- If you really want to know everything then
there is the official I2C specification.
Exercises (not graded)
-
A short description of some Uppaal exercises is
here. Homework was to read these
exercises and come up with partial solutions. That is,
while working on these exercises you will identify sub-problems.
These sub-problems may be new to you and require a trick
you don't know.
Files containing useful Uppaal templates(right-click to save) are
-
LTL exercises.
- Homework:
-
Take the model for distributed termination detection
and the formulas and then:
- Use uppaal to contruct a counter-example against the correctness. Then try to explain the problem.
- Liveness doesn't matter if there is an error, but try to check the liveness formula
anyway. Why does it take so long? Will it ever stop? Why? Possible solutions?
-
practice exam
Background reading
-
More about the specification formalism used to define the coffee machine
can be found in: F.J. van Dijk, W.J. Fokkink, G.P. Kolk, P.H.J. van de Ven and S.F.M. van Vlijmen, EURIS, a specification method for distributed interlockings, in (W. Ehrenberger, ed) Proc. 17th Conference on Computer Safety, Reliability and Security - SAFECOMP'98, Heidelberg, Lecture Notes in Computer Science 1516, pp. 296-305, Springer (October 1998).
A copy is available.
-
The tool Uppaal is installed one the ZID network in a project directory
and can be used by adding /afs/zid1.uibk.ac.at/project/c703/vmc/bin
to your PATH. (The name of the binary is uppaal.) Both the tool
and a tutorial for it can be downloaded from the
Uppaal website.
There is a local copy of the tutorial.
-
As background information on timed automata, Chapter 17 from Edmund M. Clarke, Jr., Orna Grumberg, and Doron A. Peled, Model Checking is available to registered students on
e-campus.
-
For convenience, the language reference of the online help for Uppaal is available
as a single document on
e-campus for registered students.
-
For the single process bidirectinal buffer with delay there
are an Uppaal model and
formulas.
- The material for the slides was taken from: Moshe Y. Vardi: An Automata-Theoretic Approach to Linear Temporal Logic. Banff Higher Order Workshop 1995: 238-266.
(PDF copy)
-
A little tool in OCaml byte code (so you need OCaml installed to run it)
that translates a process algebra into Uppaal.
The tool accepts specifications like
chan a
chan b,c
proc x is
X = a! . X
in X
proc y(c,d) is
Y = c? . Y + d? . Z
Z = delta
in Y
system x || y(a,a)
The tool is a filter. That is, it is called as
pa < input.pa > output.xml
The tool is a prototype, in particular the error messages are cryptic if present at all
and there is no documentation.
- Safety
- Liveness
- Use cases: formula's that show that expected behaviour is present. (A system that has no behaviour at all trivially satisfies safety formulas and liveness properties of the form if A then eventually B.)
- Correctness issues: timing requirements, status indicators working as advertised, etc.
Files containing useful Uppaal templates(right-click to save) are
-
Take the model for distributed termination detection
and the formulas and then:
- Use uppaal to contruct a counter-example against the correctness. Then try to explain the problem.
- Liveness doesn't matter if there is an error, but try to check the liveness formula anyway. Why does it take so long? Will it ever stop? Why? Possible solutions?
The tool accepts specifications like
chan a chan b,c proc x is X = a! . X in X proc y(c,d) is Y = c? . Y + d? . Z Z = delta in Y system x || y(a,a)The tool is a filter. That is, it is called as
pa < input.pa > output.xmlThe tool is a prototype, in particular the error messages are cryptic if present at all and there is no documentation.