4th International Conference of B and Z Users

University of Surrey, Guildford, UK, 13-15 April 2005
Organised by APCB and the Z User Group

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.

 Maintained by Rob Delicata.