Emerald Group Publishing Limited
Copyright © 2004, Emerald Group Publishing Limited
ZB2003 – The 3rd International Conference of B and Z Users
ZB2003 – The 3rd International Conference of B and Z Users
4-6 June 2003, Turku, Finland
B and Z are two formal methods with a common origin, and are the most popular approaches used in industry and academia for formal software development. In ZB2003, the B and Z communities came together to hold a joint conference which simultaneously incorporates the 14th International Conference of Z users and the 5th International Conference on the B method. The conference was organised by Abo Akademi University and Turku Centre for Computer Science (TUCS).
The conference attracted distinguished researchers and practitioners from both industry and academia. Three invited talks were presented, all given by celebrated researchers in formal methods. The first talk was entitled “Alloy: A Logical Modelling Language” and given by Daniel Jackson from MIT Lab for Computer Science, USA. He described a new language called “Alloy” for modelling software systems. This language shares some of the data types found in the Z language such as sets and relations, and also shares some of the concepts of Z such as the representation of system properties using simple formulas. Alloy, however, has been designed with automatic analysis in mind. A constraint solver based on reduction to SAT can check properties of alloy models and simulate execution. More information about alloy can be found at: http://sdg.lcs.edu/alloy. Formal Methods Europe sponsored the second invited talk entitled “B#: Toward a Synthesis between Z and B” given by Jean-Raymond Abrial, one of the founders of both the Z notation and the B notation. B# is a new project based largely upon the B notation and also some Z concepts. It is designed for modelling complex systems in general, not only software systems. A central idea of B# is to use the general paradigm of events to model discrete systems. The final invited talk entitled “Towards Practical Proofs of Class Correctness” was given by Bertrand Meyer from ETH Zurich. Classes and their operations can be extended by contracts that specify the intended effect of the operations. The talk described a theory, framework and process for proving that such classes satisfy their contracts. A particularly interesting aspect of the talk was the applicability of the techniques to the correctness of classes that use pointers, such as linked lists. The invited talks were given at the start of each conference day, followed by interleaved sessions on B and Z.
The first session on the first day of the conference was concerned with the topic of patterns. Patterns provide a solution to a problem in a context, promoting best practice and the sharing of expertise. Typically a pattern comprises a template or algorithm and a statement of its range of applicability. The session on patterns introduced a pattern language for formal methods in general and illustrated how patterns in B and Z may be practically used in software engineering. A session on application explored how Z and B may best be used in real world software development. In particular, it was discussed how CSP may be used to enable controlled interaction between B machines; how shortfalls in Z can be solved by using a hybrid methodology based on Z and Petri-Nets; and how event-B, a B method variant, can be used to model embedded systems with a high degree of parallelism but using as few components as possible. The next session encompassed the area of refinement in Z. Refinement is the process by which high-level abstract specifications are transformed into more concrete, low-level specifications. The session covered operation refinement theories and monotonicity; non-atomic refinement, i.e. when an abstract operation is refined into a sequence of concrete operations rather than a single concrete operation; and data refinement by forward simulation.
The second day of the conference was again a mixture of sessions on Z and B. The first session related to B theory covering topics such as backward refinement in B; the application of generalised substitutions to expressions, as well as predicates, to obtain “expression transformers”; and the introduction of probability to the B method by extending the Generalised Substitution Language with an “abstract probabilistic choice” operator. The second session dealt with model checking issues in Z. An approach to proving temporal properties of Z specifications was proposed; and a framework for the compositional verification of Object-Z specifications was presented. Object-Z is an object-oriented version of Z developed at the University of Queensland, Australia. The discussion of object orientation in Z continued into the next session. In this session, an integration between Object-Z and timed CSP was proposed, the motivation being the difficulty of implementing real-time scheduling of complex interactions; techniques were proposed for specifying object-oriented systems using the standard Z; and the formalisation of UML using first Z and secondly Object-Z were examined and compared.
The final day of the conference began with a small session on the testing of Z specifications using the semi-automatic generation of Classification Trees. The second session of the day concerned Event B. In this session, the verification of dynamic properties of reactive systems specified using B event systems was discussed. An approach was also presented to prove event ordering properties for B specifications of information systems. These properties are expressed using the EB3 notation where input event ordering properties are defined using a process algebra similar to CSP. A brief session followed in which an XML format for standard Z was proposed. The next session concentrated on applications of the B method. The formal derivation of spanning tree algorithms was considered; the use of B refinement to analyse compensating business processes was explored; and the use of B to define a medical decision support system running on a palmtop was described. The final session of the conference dealt with possible extensions to the B method. The first extension proposed was to add control flow breaks and in this way attempt to make B a more attractive development method and closer to classical languages. The second extension proposed was to increase the expressiveness of B by allowing one to specify machines whose constituent modules may change dynamically at run time.
The conference provided an excellent opportunity for the Z and B communities to meet and share their latest research. Full proceedings are available in the LNCS series: LNCS 2651 “ZB2003: Formal Specification and Development in Z and B” Didier Bert, Jonathan Bowen, Steve King, Marina Walden (Eds) ISBN 3-540-40253-5. The next conference in the series will be held at The Royal Holloway University of London in 2005.