ZB 2003: Formal Specification and Development in Z and B
These proceedings record the papers presented at the third International Conference of B and Z Users (ZB 2003), held in the city of Turku in the south of Finland. This con- rence builds on the success of the ?rst and second conferences in this series, ZB 2000, held at the University ofYork in the UK and ZB 2002, held at the Laboratoire Logiciels Systemes ` Reseaux ´ within the Institut d’Informatique et Mathematiques ´ Appliquees ´ de Grenoble (LSR-IMAG) in Grenoble, France. The location of ZB 2003 in Turku re?ects ? theimportantworkintheareaofformalmethodscarriedoutatAboAkademiUniversity andtheTurkuCentreforComputerScience(TUCS),especiallyinvolvingtheBmethod. ? In particular, Ralph-Johan Back, Professor of Computer Science at Abo Akademi U- versity and an Academy Professor at the Academy of Finland, has made an important contribution to the development of re?nement calculus, in?uential and relevant to many formal methods, including B and Z. He was an invited speaker at the previous ZB 2002 conference. B and Z are two important formal methods that share a common conceptual origin; they are leading approaches in industry and academia for the speci?cation and devel- ment (using formal re?nement) of computer-based systems. At ZB 2003 the B and Z communitiesmetonceagaintoholdathirdjointconferencethatsimultaneouslyincor- rated the 14th International Z User Meeting and the 5th International Conference on the B method. Although organized logistically as an integral event, editorial control of the joint conference remained vested in two separate but cooperating program committees that respectively determined its B and Z content, but in a coordinated manner.