ZB2005 Tutorials
Tuesday 12th April 2005
Tutorial material
All tutorials are distributing tutorial notes either in hard copy form
at the tutorial, or on the web. The mode of distribution is given
with each tutorial. If the distribution is electronic you should
download your copy before the conference.
There will be 2 tutorials in the morning and 3 tutorials in the
afternoon of the tutorial day. Tutorials 1, 2 and 3 will be split
into two parts. The tutorial schedule is as follows:
| Morning | |
| 10:00-11:30 | Tutorial 1 & 2 part 1 |
| 11:30-12:00 | Morning tea |
| 12:00-13:30 | Tutorial 1 & 2 part 2 |
| 13:30-14:30 | Lunch |
| Afternoon | |
| 14:30-16:00 | Tutorial 3 part 1 & Tutorial 4 |
| 16:00-16:30 | Afternoon tea |
| 16:30-18:00 | Tutorial 3 part 2 & Tutorial 5 |
Morning session
Tutorial 1
| Title: | Expectation-based reasoning for sequential
probabilistic programs |
| Presenter: | Carroll Morgan |
| Abstract: | |
| One of the many approaches to the formal treatment of probabilistic
programs is the use of real-valued rather than Boolean-valued predicates
for assertions. These "probabilistic predicates", which we call
"expectations", generalise Hoare-, Dijkstra- and
B- style semantics in the same way: rather than assure a program will achieve a postcondition from some precondition, instead one assures that the "weighted average" of the real-valued "post-expectation" will never be less than a certain initial-state-dependent minimum.
This generalises the usual approach, provided we identify true/false with
1/0, since then we have false £ true: and the weighted average of a
postcondition over a single final state is just one if the state satisfies
the postcondition and zero otherwise. The correctness condition then
requires that the postcondition is one if the precondition was.
However the real-valued expectations allow much more: they can be used to
specify and/or validate a program's probability of achieving a
postcondition and -more generally still- they can be used to describe
the "cost" (or some other quantified measure) of running a program.
In this tutorial the basics of this relatively new
approach will be introduced, and its application toB and/or Z. |
| Tutorial slides: | http://www.cse.unsw.edu.au/~carrollm/ZB2005/. |
Tutorial 2
| Title: | ProB: A Verification and Validation Tool for the B method |
| Presenter: | Michael Leuschel, Michael Butler and Stephane Lo Presti |
| Abstract: | |
| ProB is an animator and a model checker for the B
Method. It allows fully automatic animation of many B specifications,
and can be used to systematically check a specification for errors. |
| The tutorial consists of three parts. We first give an overview of
the basic features of ProB. The second part is an interactive
demonstration of ProB, going through various examples in detail. We
also discuss potential pitfalls and how B machines can be rewritten to
be more suitable for animation and verification. In the last part, we
will explore advanced modes of ProB, including the integration with
CSP and constraint-based model-checking. |
| Material: | Slides and a ProB manual will be distributed. The
presenters will assist with the installation of ProB on attendees'
machines. |
| Tutorial notes: | http://www.ecs.soton.ac.uk/~splp/prob/tutorial/ |
| Reference: | http://www.ecs.soton.ac.uk/~mal/systems/prob.html |
| Demonstration: | The tools will be demonstrated during the
conference.
|
Afternoon session
Tutorial 3
| Title | Case study of a complete reactive system in Event-B:
A Mechanical Press Controller |
| Presenter | Jean-Raymond Abrial |
| Abstract | |
| A development of a complete case study ranging
from the writing of the initial English Requirement Document to the
final Simulation of the complete system (translated into C from the
last Event-B refinement). |
| Part 1: presentation of the case study and demonstration of how to
write the corresponding Requirement Document. |
| Part 2: we shall see by which methodology we can develop the
system from its initial very abstract model down to the final model
comprising about 20 sensors, 3 actuators, 5 clocks, 7 buttons, 3
operating devices, 5 operating modes, 7 emergency situations, etc. |
| Requirements: | http://www.zb2005.org/PRESS-req-doc.ps |
| The requirements will be required during the tutorial and you may
wish to download and perhaps print. |
| Tutorial slides: | The slides are available at
http://www.zb2005.org/PRESS-slides.tar.gz. |
| Source-code: | The Requirement Document, B
development, and the Simulator can be found at |
| http://www.zb2005.org/PRESS.tar.gz |
| Please see the readme file. |
Tutorial 4
| Title | Developing Z Tools with CZT |
| Presenters': | Mark Utting & Petra Malik |
| Abstract: | |
| This tutorial will give an introduction to the
architecture of the Community Z Tools Java framework and show how it
can easily be used to create new Z tools. Some experience with
programming in Java or other object-oriented languages will be
assumed. |
| The Community Z Tools (CZT) project provides an open-source Java
framework for building formal methods tools for Z and Z dialects. The
CZT project was proposed by Andrew Martin in 2001, with the goal of
providing an open Internet-based community project that survives
individuals, research projects, companies, etc. The presenters of
this tutorial initiated the development of a Java framework on
czt.sourceforge.net, and several people from various countries have
joined the project and started writing new Z tools.
CZT now includes a set of tools for parsing, type-checking,
transforming and printing standard Z specifications in LATEX, Unicode
or XML formats. This tutorial gives an overview of the CZT framework,
shows how to use the standard components such as parsers and
type-checkers with just a few lines of Java code, and how to use the
CZT visitor design pattern to traverse and transform Z specifications. |
| Tutorial slides: | Printed copies of the slides will be
available after the tutorial |
| Software: | CZT software is available at http://czt.sourceforge.net. |
| The software can be downloaded and installed prior to attending the
conference. Assistance with installation of software will be
available during the other days of the conference. |
| Demonstration: | The tools will be demonstrated during the
conference. |
Tutorial 5
| Title: | Model-Based Testing using Formal Models From Theory
to Industrial Applications |
| Presenters: | Bruno Legeard & Mark Utting |
| Abstract: | The main objectives of this tutorial are to
introduce the techniques of automated functional black-box test
generation from formal models and to show on the basis of industrial
applications how it is effective to validate critical software. |
| After two decades of intensive research in using formal
specifications for test generation purpose, these techniques reach a
first maturity level: various successful experiments have been
realized and environments start to be available both academics and
commercials. Indeed, formal model-based testing really breaks the
traditional practices in functional black-box testing and offers new
solutions to face the growing complexity of the system to be
validated. More precisely, it offers the opportunity to give a
rational for better covering the requirements and it allows reducing
the cost of test design. In this tutorial, we introduce the formal
model-based techniques and we show on the basis of various industrial
application presentations the advantages, difficulties and drawbacks
of such techniques. This tutorial takes benefit from the experience of
the authors in developing the formal model-based generator
BZ-Testing-Tools, now industrialized by the company Leirios
Technologies and using it in several industrial applications in
various domains of critical software (Smart Card, Automobile software,
urban systems, etc) |
| Tutorial slides: | Printed copies of the slides will be
available after tutorial |
| Demonstration: | The tools will be demonstrated during the
conference. |
|
|
