[Apologies for multiple copies]
[Don't forget to register to the conference]
------------------------------------------------------------------------
ZB2002
2nd Int. Conference of Z and B Users
23-25 January 2002
Grenoble, France
http://www-lsr.imag.fr/zb2002/
Tuesday 22 January 2002: Program of Tutorials and Education Session
------------------------------------------------------------------------
10h-12h: The RSDS/B Method and Tools
K. Lano, D. Clark, K. Androutsopoulos
Department of Computer Science
King's College, London, U.K.
This tutorial will describe the RSDS method and its supporting tools,
which provide a means of generating B specifications and
implementations from UML notations such as state machines, invariants
and class diagrams. RSDS also provides a bridge between implicit
Z-style specifications and explicit B designs and implementations.
The method provides guidelines for structuring and decomposing
specifications, and for the incorporation of scheduling algorithms
and fault tolerance strategies. RSDS has been used for many examples
of reactive systems such as the production cell and steam boiler case
studies, and has been used in the process industry for the synthesis
of a control system for a milk pasteurisation plant.
The RSDS tools support hazard analysis of UML class diagrams and
system physical layout diagrams; the construction of state
machine/invariant specifications of reactive systems and the
consistency and completeness checking of these; the decomposition of
specifications into smaller subsystem specifications, and the
synthesis of control algorithms from invariants. Translators to B,
Java and SMV are provided, to enable checking of static and temporal
properties and to provide executable implementations of a control
system.
---------------------------------------------------------------------
14h-14h30:
Jean-Louis Boulanger
RATP - De'partement E.S.T. Inge'nierie du Transport Ferroviaire
Vincennes, France
Georges Mariano
INRETS, France
The goal of this presentation is to show how it is possible, taking
the field of digital (simple) circuits design as a case study, to
explain the basic concepts of the B formal method.This tutorial in
intended to be provided in a short cursus (near 10 hours), it is
concrete and covers all the main stages of the B formal process.Taking
a model of the digital circuit and his refinement, proof obligations
are automatically generated and may be discharged using an automatic B
dedicated prover. This way, it is proved that a more concrete model is
correct with respect to the more abstract one. Thus, it's proved at
the end of the process that the implementation is correct with respect
to the initial and abstract specification. More precisely, starting
from a functional (and logical) specification of a digital circuit,
the corresponding abstract B model is built. Then, the refinement
steps are used mainly to define how the circuit will be implemented
over already available (but at lower level) models. In B parlance,
basic models are provided for simple circuits (logical gates but also
transistors) in order to be reusable when implementing the targeted
circuit.
---------------------------------------------------------------------
14h30-15h: Specification and refinement using B: Two pedagogical examples
Marc Guyomard
Enssat/IRISA (Cordial)
Universite' de Rennes I
Lannion , France
Despite the fact that its relevance in programming design was
identified a long time ago, the notion of refinement has met with some
difficulties in becoming a common practice. The main reasons for that
lie in the weakness of specification formalisms as well as in the lack
of formal tools for checking the consistency between specification and
refinement. From this standpoint Method B offers promising prospects
as illustrated by two tutorial class drills. The first one shows how
strengthening techniques allow us to refine without losing
efficiency. The second one shows how it is both possible and relevant
to work with two different representations of the same concept.
---------------------------------------------------------------------
15h-15h30: Some (beneficial) side effects of Z and B learning.
Jean-Yves Lafaye
Dpt Informatique, Universite' La Rochelle.
Laboratoire L3i
La Rochelle, France
We first intend to present a series of plain examples that are the
basis of a course on Z an B for a second year IUT (= polytechnics)
class. After screening the main objectives of the course, we'll
discuss how students (say they) feel about it, and which are the
results. We'll also discuss how other teachers in mathematics,
software engineering, database, testing ... are more or less involved
in a practical cooperation with formal specification teachers.
---------------------------------------------------------------------
15h30-16h: Development of atomic memory protocols.
Mamoun Filali
IRIT Universite Paul Sabatier
Toulouse, France
In this study we present the refinement based development of atomic
memory protocols. The goal of these protocols is to manage concurrent
accesses to shared data. The abstract view of such protocols consists
in a register with read and write operations. In order to implement
multiprocessor bus based protocols, we introduce successive
refinements leading to well known protocols (Illinois, Firefly, ...).
---------------------------------------------------------------------
16h30-18h:
Ken Robinson
School of Computer Science & Engineering
UNSW, Australia
In the Software Engineering program at UNSW, we run Software
Engineering workshops across the first three years. In the two second
year workshops we have incorporated B into the specification, design
and implementation of a prototype. Currently these projects are
undertaken by 150 students split into teams of approx 4.
In the first workshop, a B specification is developed in parallel with
the use of DFD and Use Cases. The specification is demonstrated using
the animator in the B Toolkit.
In the second workshop, an OO design is developed from the B
specification, in which the B machines are associated with classes in
the OO class diagram. The specification is then implemented using the
Base generator of the B Toolkit and the C code from the translation
produced by the B Toolkit is embedded, for example using JNI (Java
Native Interface), into the OO implementation of the prototype.
This presentation will demonstrate an example of the type of project
produced by students, and will discuss experiences and plans for the
future. These plans include modification of the B Toolkit to
facilitate the process.
---------------------------------------------------------------------
18h-18h30: Examination question instances. Comments on the results
Henri Habrias
Departement informatique, IUT de Nantes, IRIN
Universite' de Nantes, France
We present exercises we designed in order to test the understanding
level of students. One treats of the way students find out errors in
syntax and semantics.
Experiences in B-notation applied to various domains (law, text
analysis ...) We also present instances of using B for specifications
in various matters (law, econometrics etc)
=========================================================================
|
