ZB 2003: Formal Specification and Development in Z and B: Third International Conference of B and Z Users, Turku, Finland, June 4-6, 2003, Proceedings (Lecture Notes in Computer Science (2651))

This book constitutes the refereed proceedings of the Third International Conference of Z and B Users, ZB 2003, held in Turku, Finland in June 2003. The 28 revised full papers presented together with 3 invited papers were carefully reviewed and selected for inclusion in the book. The book documents the recent advances for the Z formal specification notation and for the B method, spanning the full scope from foundational, theoretical, and methodological issues to advanced applications, tools, and case studies. 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. Alloy: A Logical Modelling Language -- An Outline Pattern Language For Z: Five Illustrations And Two Tables -- Patterns To Guide Practical Refactoring: Examples Targetting Promotion In Z -- Reuse Of Specification Patterns With The B Method -- Composing Specifications Using Communication -- When Concurrent Control Meets Functional Requirements, Or Z + Petri-nets -- How To Diagnose A Modern Car With A Formal B Model? -- Parallel Hardware Design In B -- Operation Refinement And Monotonicity In The Schema Calculus -- Using Coupled Simulations In Non-atomic Refinement -- An Analysis Of Forward Simulation Data Refinement -- B#: Toward A Synthesis Between Z And B -- Introducing Backward Refinement Into B -- Expression Transformers In B-gsl -- Probabilistic Termination In B -- Probabilistic Invariants For Probabilistic Machines -- Proving Temporal Properties Of Z Specifications Using Abstraction -- Compositional Verification For Object-z -- Timed Csp And Object-z -- Object Orientation Without Extending Z -- Comparison Of Formalisation Approaches Of Uml Class Constructs In Z And Object-z -- Towards Practical Proofs Of Class Correctness -- Automatically Generating Information From A Z Specification To Support The Classification Tree Method -- Refinement Preserves Pltl Properties -- Proving Event Ordering Properties For Information Systems -- Zml: Xml Support For Standard Z -- Formal Derivation Of Spanning Trees Algorithms -- Using B Refinement To Analyse Compensating Business Processes -- A Formal Specification In B Of A Medical Decision Support System -- Extending B With Control Flow Breaks -- Towards Dynamic Population Management Of Abstract Machines In The B Method. Edited By Didier Bert, Jonathan P. Bowen, Steve King, Marina Waldén. Alloy: A Logical Modelling Language....Pages 1-1 An Outline Pattern Language for Z: Five Illustrations and Two Tables....Pages 2-19 Patterns to Guide Practical Refactoring: Examples Targetting Promotion in Z....Pages 20-39 Reuse of Specification Patterns with the B Method....Pages 40-57 Composing Specifications Using Communication....Pages 58-78 When Concurrent Control Meets Functional Requirements, or Z + Petri-Nets....Pages 79-97 How to Diagnose a Modern Car with a Formal B Model?....Pages 98-100 Parallel Hardware Design in B....Pages 101-102 Operation Refinement and Monotonicity in the Schema Calculus....Pages 103-126 Using Coupled Simulations in Non-atomic Refinement....Pages 127-147 An Analysis of Forward Simulation Data Refinement....Pages 148-167 B # : Toward a Synthesis between Z and B....Pages 168-177 Introducing Backward Refinement into B....Pages 178-196 Expression Transformers in B-GSL....Pages 197-215 Probabilistic Termination in B ....Pages 216-239 Probabilistic Invariants for Probabilistic Machines....Pages 240-259 Proving Temporal Properties of Z Specifications Using Abstraction....Pages 260-279 Compositional Verification for Object-Z....Pages 280-299 Timed CSP and Object-Z....Pages 300-318 Object Orientation without Extending Z....Pages 319-338 Comparison of Formalisation Approaches of UML Class Constructs in Z and Object-Z....Pages 339-358 Towards Practical Proofs of Class Correctness....Pages 359-387 Automatically Generating Information from a Z Specification to Support the Classification Tree Method....Pages 388-407 Refinement Preserves PLTL Properties....Pages 408-420 Proving Event Ordering Properties for Information Systems....Pages 421-436 ZML: XML Support for Standard Z....Pages 437-456 Formal Derivation of Spanning Trees Algorithms....Pages 457-476 Using B Refinement to Analyse Compensating Business Processes....Pages 477-496 A Formal Specification in B of a Medical Decision Support System....Pages 497-512 Extending B with Control Flow Breaks....Pages 513-527 Towards Dynamic Population Management of Abstract Machines in the B Method....Pages 528-545