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.
Author(s): Daniel Jackson (auth.), Didier Bert, Jonathan P. Bowen, Steve King, Marina Waldén (eds.)
Series: Lecture Notes in Computer Science 2651
Edition: 1
Publisher: Springer-Verlag Berlin Heidelberg
Year: 2003
Language: English
Pages: 554
Tags: Software Engineering; Logics and Meanings of Programs; Mathematical Logic and Formal Languages
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
