Didier Bert / Jonathan P. Bowen / Steve King / Marina Waldén (eds.)

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
Herausgegeben:Bert, Didier; Bowen, Jonathan P.; King, Steve; Walden, Marina

• Broschiertes Buch

Produktbeschreibung

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.

Produktdetails

• Lecture Notes in Computer Science 2651
• Verlag: Springer / Springer Berlin Heidelberg / Springer, Berlin
• Artikelnr. des Verlages: 978-3-540-40253-4
• 2003
• Seitenzahl: 568
• Erscheinungstermin: 20. Mai 2003
• Englisch
• Abmessung: 235mm x 155mm x 31mm
• Gewicht: 840g
• ISBN-13: 9783540402534
• ISBN-10: 3540402535
• Artikelnr.: 14804085

Autorenporträt

Didier Bert, CNRS, Saint-Martin-d'Heres Cedex, France / Jonathan P. Bowen, South Bank University, London, UK / Steve King, University of York, UK / Marina Waldén, Abo Akademi University, Turku, Finland

Inhaltsangabe

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.