Notice of Conference and 2nd Call for Participation ZUM'98 11th International Conference of Z Users Organized by the Z User Group In cooperation with Daimler-Benz Research Berlin, GMD and TU Berlin Sponsored by Daimler-Benz and Praxis Critical Systems Supported by BCS-FACS Berlin, Germany 24-26th September 1998 The 11th International Conference of Z Users (ZUM'98) will be held at Berlin, Germany, 24-26 September 1998. The following invited speakers will give presentations at the conference: Dr. Klaus Grimm (Daimler-Benz AG, Germany) Prof. Nancy Leveson (University of Washington, USA) Prof. Dr. Ernst-Ruediger Olderog (Universitat Oldenburg, Germany) Ib Sorensen (B-Core(UK) Limited, UK) The conference will also include: Tool demonstrations Exhibitions by publishers Posters or leaflets Attendees will receive a copy of the proceedings, to be published by Springer-Verlag Lecture Notes in Computer Science, as part of the delegate pack. To attend, please complete and return the booking forms with the appropriate remittance or credit card information. We look forward to seeing you at the meeting. For up-to-date on-line information about the conference, see: http://www.fmse.cs.reading.ac.uk/zum98/ Programme committee: Ali Abdallah, The University of Reading, UK Jonathan Bowen, The University of Reading, UK Paolo Ciancarini, University of Bologna, Italy Neville Dean, Anglia Polytechnic University, UK John Derrick, The University of Kent at Canterbury, UK Mark d'Inverno, University of Westminster, UK Andy Evans, University of Bradford, UK Andreas Fett, Daimler-Benz Research Berlin, Germany (local org) David Garlan, Carnegie-Mellon University, USA Wolfgang Grieskamp, TU Berlin, Germany (local org coordinator) Henri Habrias, University of Nantes, France Jonathan Hammond, Praxis Critical Systems, UK Ian Hayes, University of Queensland, Australia Stephan Herrmann, GMD, Germany (local org) Mike Hinchey, NJIT, USA & University of Limerick, Ireland Hans-Martin Hoercher, Vossloh System-Technik GmbH, Germany Jonathan Jacky, University of Washington, USA Stephan Jahnichen GMD & TU Berlin, Germany (local org) Randolph Johnson, National Security Agency, USA Kevin Lano, Imperial College, London, UK Shaoying Liu, Hiroshima City University, Japan Jean-Francois Monin, France Telecom CNET DTL/MSV, France Peter Pepper, TU Berlin, Germany (local org) Norah Power, University of Limerick, Ireland Alf Smith, DERA Malvern, UK David Till, City University, London, UK Sam Valentine, University of York, UK Matthias Weber, Daimler-Benz Research Berlin, Germany (local org) Jim Woodcock, Oxford University, UK John Wordsworth, IBM Hursley UK Laboratories, UK Local information The city of Berlin is located at the very centre of Europe, close to the border with Poland (distance 100 km) and the Czech Republic (250 km). The conference takes place at the campus of the Technische Universitat Berlin (TUB). With around 37,000 students, the TUB is the largest technical university in Germany. Teaching and research in the TUB computer science department focus on software and communication technology, with a strong tradition regarding formal methods, in particular using algebraic specification. The TUB campus is located within the inner city of Berlin, around 20 minutes walking distance (through the central park Tiergarten) from the Brandenburg Gate (Brandenburger Tor) and the Potsdamer Platz. The picture shows a view on the campus, with Tiergarten in the background, and the Street of the 17th June, leading directly to the Brandenburg Gate. Travel Berlin has good road and rail connections, and offers access by air via the three international airports: Tegel, Schvnefeld, and Tempelhof. Flights from western Europe usually arrive at Tegel to the north of central Berlin. From there to the inner city via taxi costs around 30 DM. Coaches (bus line 109) to the main railway station Zoologischer Garten, which is near to the conference venue, are also available. Accommodation We have made special arrangements with three hotels in the inner city of Berlin: Hotel A. Berlin Excelsior Hotel, Hardenbergstr. 14, 10623 Berlin. Tel: +49+30-3155-0, Fax: +49+30-3155-1002. Located in the south of the TUB campus, only a few minutes by foot from the conference venue. Price: 171/222 DM per night for a single/double room. Directions: From the Tegel airport, take the airport coach (bus line 109) to the main railway station Zoologischer Garten. From there it takes about 5-10 minutes by foot. From the Schvnefeld airport, there is an S-Bahn (city rail) to Zoologischer Garten. Hotel B. SORAT Art'otel Berlin, Joachimstalerstr. 29, 10719 Berlin, Tel: +49+30-8844470, Fax: +49+30-88447700. Located very near to the Kurfurstendamm, the famous shopping boulevard of Berlin, and to the the main railway station, Zoologischer Garten. About 15-20 minutes by foot to the conference venue. Alternatively, take the underground U2 from Zoologischer Garten, direction Ruhleben, to the next station, Ernst-Reuter Platz. Price: 161/197 DM per night for a single/double room. Directions: From the Tegel airport, take the airport coach (bus line 109) to the central railway station Zoologischer Garten. Get off at "Joachimstaler Strasse" and walk back about 200 metres. From the Schvnefeld airport, there is an S-Bahn (city rail) to Zoologischer Garten. From there it takes about 5 minutes by foot. Hotel C. Hotel unter den Linden, Unter den Linden 14, 10117 Berlin. Tel: +49+30-238110, Fax: +49+30-2811100. Located at the representative boulevard Unter den Linden, in the eastern central city (Berlin Mitte), where the new government area is to be found. Around 10 minutes using the underground U2, starting at station Mohrenstr., direction Ruhleben, to the conference venue, station Ernst-Reuter Platz. Price: 116 DM per night for a single room (double rooms not available). Directions: From the Tegel airport, take the airport coach to the central railway station Zoologischer Garten. From there take U2, direction Vinetastr., to the station Mohrenstr. From Schvnefeld, there is an S-Bahn (city rail) to the railway station Friedrichstrasse, which is near to "Unter den Linden". Rooms need to be reserved using a separate hotel booking form. The advertised prices for hotels can be offered during the period starting two days before and finishing two days after the main conference. Conference events A reception is planned on Wednesday evening. There will be a conference banquet on Thursday, which is included in the registration fee. Extra places can be reserved if required. On Friday evening there is an optional guided tour on foot to the Potsdamer Platz area, the so-called Schaustellentour ("Schau-stelle" is an artificial word derived from "Bau-stelle", where Baustelle means construction area, and "Schau" means just show). The tour offers a mixture of historical and architectural information (Brandenburger Tor, Reichstag, Wilhelmstrasse, and so on - the political centre of the 2nd and 3rd German Reich) with information about the newly constructed government and business area located there. The tour is on foot and will take approximately 2 hours. For a dinner following the tour, restaurants in the area will be recommended. ZUM'98: Contact information Conference Chair: General enquiries about the conference may be directed to: Mike Hinchey Department of Computer Science College of Information Science and Technology, University of Nebraska at Omaha 6001 Dodge Street, Omaha, NE 68182-0500, USA Email: mhinchey@unomaha.edu Tel: +1-402-554-4996 Fax: +1-402-554-2975 Programme Co-Chairs: Jonathan Bowen The University of Reading, Department of Computer Science Whiteknights, PO Box 225, Reading, Berks RG6 6AY, UK Tel: +44-118-931-6544 Fax: +44-118-985-1994 Email: J.P.Bowen@reading.ac.uk Andreas Fett Daimler-Benz AG Alt-Moabit 96a, Berlin, Germany Tel: +30-39982-209 Fax: +30-39982-107 Andreas.Fett@dbag.bln.DaimlerBenz.com Local organization and Tool Demonstrations For information concerning tool demonstrations and general local organization contact: Wolfgang Grieskamp TU Berlin, Germany Email: wg@cs.tu-berlin.de Stephan Herrmann GMD, Germany sh@first.gmd.de For details concerning publishers' stands, leaflets and posters, or any other queries, please contact Mike Hinchey (contact information above). Tutorials For information concerning tutorials, please contact: David Till City University, UK Email: till@soi.city.ac.uk Educational issues session Neville Dean (ZUGEIS Organizer) Anglia Polytechnic University Applied Sciences, East Road, Cambridge CB1 1PT, UK Email: c.n.dean@anglia.ac.uk Tel: +44-1223-363271 ext 2329 Fax: +44-1223-352989 A separate mailing list related to the meeting, and acting as a forum for educators and others to discuss related areas, is available. To subscribe, email to zugeis-request@comlab.ox.ac.uk including your name and address and a brief statement of your interests. Tutorials and registration provisional timetable Wednesday, 23rd September 1998 13:00 Tutorial registration / Lunch 14:00 Developing Safety-Critical Embedded Systems: The ESPRESS Approach (Wolfgang Grieskamp et al., Germany) 15:30 Coffee Break 17:30 Close 14:00 Effective Use of Z/EVES (Mark Saaltink, Canada) 15:30 Coffee Break 17:30 Close ev. Conference registration / Reception Note: tutorials will only take place if sufficient numbers book. Further tutorial information is available below. ZUM'98 provisional programme: 24-26th September 1998 Thursday, 24th September 1998 09:00 Registration / Coffee 09:30 Welcome (Chair: Mike Hinchey) 09:30 Opening remarks -- Mike Hinchey, University of Limerick, Ireland 09:45 INVITED SPEAKER Industrial Requirements for the Efficient Development of Reliable Embedded Systems -- Klaus Grimm, Daimler-Benz AG, Germany 10:30 Coffee Break 11:00 Concurrency (Chair: Wolfgang Grieskamp) 11:00 How to Combine Z with a Process Algebra -- C. Fischer, Germany 11:30 The Specification and Refinement of an Environmental Model -- W.J. Stoddart, UK 12:00 Formal Derivation of Finite State Machines for Class Testing -- L. Murray, D. Carrington, I. MacColl, J. McDonald and P. Strooper, Australia 12:30 Lunch 14:00 Tools (Chair: Andreas Fett) 14:00 INVITED SPEAKER Using B to Specify, Verify and Design Hardware Circuits -- Ib Sorensen, B-Core(UK) Limited, UK 14:45 Z on the Web Using Java -- J.P. Bowen and D. Chippington, UK 15:05 Visualizing Z Notation in HTML Documents -- P. Ciancarini, C. Mascolo and F. Vitali, Italy 15:30 Coffee Break 16:00 Z and HOL (Chair: Stephan Herrmann) 16:00 On the Semantic Relation of Z and HOL -- T. Santen, Germany 16:30 HOL-Z in the UniForM-Workbench - A Case Study in Tool Integration for Z -- C. Luth, E. W. Karlsen, Kolyang, S. Westmeier and B. Wolff, Germany 17:00 AGM of the Z User Group (Chair: Jonathan Bowen) 17:30 Close 19:30 Conference Banquet Friday, 25th September 1998 09:15 Safety-Critical and Real-Time Systems (Chair: Mike Hinchey) 09:15 INVITED SPEAKER Designing a Requirements Specification Language for Reactive Systems -- Prof. Nancy Leveson, University of Washington, USA 10:00 Analyzing a Real-Time Program with Z -- J. Jacky, USA 10:30 Coffee Break 11:00 Theory (Chair: Sam Valentine) 11:00 Recursive Definitions in Z -- R.D. Arthan, UK 11:30 A Logic for the Schema Calculus -- M.C. Henson and S. Reeves, UK/New Zealand 12:00 Tool demonstrations 12:30 Lunch 14:00 Theory and Standards (Chair: Jonathan Bowen) 14:00 INVITED SPEAKER Combining Specification Techniques for Processes, Data and Time -- Prof. Ernst-Ruediger Olderog, University of Oldenburg, Germany 14:45 Innovations in the Notation of Standard Z -- I. Toyn, UK 15:15 Coffee Break 16:00 Issues (Chair: Neville Dean) 16:00 Comparing Extended Z with a Heterogeneous Notation for Reasoning about Time and Space -- R.F. Paige, Canada 16:30 Inconsistency and Undefinedness in Z - A Practical Guide -- S.H. Valentine, UK 17:00 Close 17:30 Optional guided tour (followed by dinner) Saturday a.m., 26th September 1998 09:00 Refinement (Chair: David Till) 09:00 Compositional Specification of Controllers for Batch Process Operations -- K. Lano, P. Kan and A. Sanchez, UK 09:30 Testing Refinements by Refining Tests -- J. Derrick and E. Boiten, UK 10:00 More Powerful Z Data Refinement: Pushing the State of the Art in Industrial Refinement -- S. Stepney, D. Cooper and J.C.P. Woodcock, UK 10:30 Coffee Break 11:00 Object Orientation (Chair: John Derrick) 11:00 Network Topology and a Case Study in TCOZ -- B. Mahony and Jin Song Dong, Australia 11:30 Object-Oriented Specification of Hybrid Systems Using UMLh and ZimOO -- V. Friesen, A. Nordwig and M. Weber, Germany 12:00 Translating the OMT Dynamic Model into Object-Z -- S. Dupuy, Y. Ledru and M. Chabre-Peccoud, France 12:30 Final Remarks and Best Paper Vote -- Mike Hinchey 12:45 Close ZUM'98 Educational Issues Session Saturday p.m., 26th September 1998 Organizer: Neville Dean, Anglia Polytechnic University, UK Note that the session will be informal giving an opportunity for discussion. 13.00 Lunch 14:00 Introduction -- Neville Dean, UK What and How to Teach (Chair: Mike Hinchey, Ireland/US) 14:05 Z on the Web -- Jonathan Bowen, UK 14:30 Mental models of Z -- Neville Dean, UK 15:00 What makes a good specification case study? (Panel Discussion) -- Norah Power, Ireland 15:30 Coffee Break 16:00 Assessment Issues (Chair: Neville Dean, UK) 16:00 Collaborative work to answer a test on formal specification in B -- Henri Habrias, France 16:30 Managing Z coursework on-line -- Zarina Shukur, Edmund Burke and Eric Foxley, UK 17:00 General discussion 17:20 Concluding remarks 17:30 Close ZUM'98 tutorials Wednesday, 23rd September 1998 TUTORIAL A: Developing Safety-Critical Embedded Systems: The ESPRESS Approach Presenters: Wolfgang Grieskamp (1), Maritta Heisel (2), Thomas Santen (3) and Matthias Weber (4) (1) Technische Universitat Berlin (2) Otto-von-Guericke Universitat Magdeburg (3) GMD FIRST (4) Daimler-Benz AG ESPRESS is an application-oriented German project which aims to develop a software technology for the construction of safety-critical embedded systems. Sponsored by the German ministry of education and research, BMBF, the project is a cooperation between Daimler-Benz AG, Robert Bosch AG, the Fraunhofer Gesellschaft, GMD Gesellschaft fur Mathematik und Datenverarbeitung and the Technische Universitat Berlin. The tutorial gives an overview of the ESPRESS approach. Illustrated by one of the ESPRESS case studies, an intelligent cruise control system, the development of a requirements specification using a combination of Statecharts and the Z notation will be presented in detail. Validation techniques based on this specification will be explained. Specific topics include: * Agendas, which provide a methodological concept for representing process knowledge for particular software architectures on a fine-grained level of detail. * The notation mSZ, which combines the formalisms Statecharts, Z, and temporal logic for the specification of safety-critical reactive systems. * Validation techniques based on the Isabelle/HOL-Z tool, including verification of certain aspects of a specification, and generation of test cases. * An online tool demonstration, showing the integration of commercial tools such as Statemate with the ESPRESS tools for editing, type-checking, and validating Z and mSZ specifications. The tutorial is aimed at practitioners and researchers interested in the requirement specification of reactive and embedded systems. Basic knowledge about formal methods and Z is assumed. Contact Wolfgang Grieskamp (email wg@cs.tu-berlin.de) for further information. TUTORIAL B: Effective Use of Z/EVES Presenter: Mark Saaltink, ORA, Canada This half-day tutorial will show how to use mechanical assistance in the analysis of some large Z specifications. Among the areas we will highlight are: * the use of sections. Using the proposed ISO Z sections mechanism lets us divide a specification into reusable generic parts and a parts specific to the problem at hand. * the automation of simple inferences. Z/EVES allows its users to mark theorems for automatic use. Doing so properly allows the prover to look after the trivial, leaving the user free to focus on the main issues in a proof. * pitfalls of proofs in Z. Z is supposed to allow for a fairly conventional approach to discrete mathematics. In the area of generics it falls short of this goal. We explain the problem, show how it affects Z/EVES, and discuss solutions. Participants should come with a reasonably good understanding of Z and some interest in proofs, and should leave with an interest in Z/EVES and an understanding of ways to present their specifications to facilitate proofs. Detailed topics will include: a review of Z/EVES capabilities, a discussion of sections, as proposed for ISO standard Z, a discussion of proofs, both informal and formal, a presentation of a section, an analysis of parts of a specification, and a discussion of proof pitfalls. Contact Mark Saaltink (email mark@ora.on.ca) for further information. Bookings Please complete the conference booking form and hotel booking form below as required and send them by fax (preferably) or postal mail to: BWO Marketing Service GmbH ZUM'98 Mohrenstrasse 63-64 10117 Berlin Germany Fax: +49+30-22668464 Email: drooff@ibm.net (c/o Stephan Drooff) Booking for the conference and for hotels can be made by email and payment made at registration (using a Mastercard/Visa credit card or in German DM cash). NOTE: FOR SECURITY DO NOT EMAIL CREDIT CARD DETAILS. Only send credit card details by fax or postal mail. Those who would like to pay by cheque send the cheques (noting the usual restrictions on amount) with the booking forms. There is no fee for using EuroCheques, but we have to charge a fee of 25 DM for processing foreign cheques (please add this fee to the amount). If you require an invoice for your booking, there is an administration charge (see the conference booking form). Important: please send different cheques for conference booking and for hotel booking. For the conference booking, make the cheque payable in German DM to "BWO Marketing Service GmbH". For the hotel booking, make the cheque payable in German DM to "DER" (Deutsches Reiseburo). You will receive an acknowledgment for the actual reservation - according to availability and your first and second hotel choice. CONFERENCE BOOKING FORM: _______________________________________________________________________________ | ZUM'98 Conference Booking Form, 11th International Conference of Z Users | | Berlin, Germany, 24-26 September 1998 | | | |Surname ..................... First name .................... Title .......| | | |Organization ................................................................| | | |Address .....................................................................| | | |.............................................................................| | | |Postcode .................... Country ......................................| | | |Telephone ................. Fax ................. Email ...................| | | |Arrival Date ........................ Departure Date .......................| | | |Please indicate any dietary or other requirements: | | | |Vegetarian? ................... Other ......................................| |_____________________________________________________________________________| |Main conference, Thursday - Saturday am, 24-26 September, including | | |lunch on Thursday/Friday, refreshments, conference dinner on Thursday | | |and proceedings. 600 DM | | |______________________________________________________________________|______| |Tutorials (including lunch and refreshments): | | |Wednesday 23 September 200 DM | | | ____ ____ | | |Please tick tutorial required: Tutorial A |__| Tutorial B |__| | | |______________________________________________________________________|______| |Education Session (Saturday pm, 26 September): | | |(including lunch and refreshments) 75 DM | | |______________________________________________________________________|______| |Extras (subject to availability): | | |Extra ticket for conference dinner (Thursday night) 120 DM | | |Optional guided tour excursion (Friday night) 10 DM | | |Invoice request 30 DM | | |______________________________________________________________________|______| |Discounts: (Please note, only one discount allowed) | | |BCS FACS members -30 DM | | |Authors (one per published paper) -100 DM | | |______________________________________________________________________|______| |Total amount due (in German DM): | DM | | |_____________________| | ____ ____ | |Credit card: Mastercard |__| Visa |__| (ONLY BY FAX / POSTAL MAIL) | | | |Card Number ......../......../......../........ Expiry Date ................| | | |Holder ......................................................................| | | |Signature ..................................... Date .......................| | | |Comment (other payment method) ..............................................| | | |.............................................................................| |_____________________________________________________________________________| HOTEL BOOKING FORM: _______________________________________________________________________________ | ZUM'98 Hotel Booking Form, 11th International Conference of Z Users | | Berlin, Germany, 24-26 September 1998 | | | |Surname ..................... First name .................... Title .......| | | |Organization ................................................................| | | |Address .....................................................................| | | |.............................................................................| | | |Postcode .................... Country ......................................| | | |Telephone ................. Fax ................. Email ...................| |-----------------------------------------------------------------------------| | A B C | |Hotel first choice: |__| |__| |__| | | | |Hotel second choice: |__| |__| |__| | | | | Single Double | |Room |__| |__| with: ...................| | | |Arrival date ........................ Departure date .......................| | | |Arrival later than 6pm ............... Number of nights .....................| | | |Further comments ............................................................| | | |.............................................................................| |_____________________________________________________________________________| |Payment Euro-/Mastercard Visa Diners | | |__| |__| |__| | | | |Card Number ......../......../......../........ Expiry Date ................| | | |Holder ......................................................................| | | |Signature ..................................... Date .......................| | | |Comment (other payment method) ..............................................| | | |.............................................................................| |_____________________________________________________________________________| Information provided by Jonathan Bowen and Wolfgang Grieskamp