ZB 2003: Formal Specification and Development in Z and B (eBook, PDF)

Third International Conference of B and Z Users, Turku, Finland, June 4-6, 2003, Proceedings
Redaktion: Bert, Didier; Waldén, Marina; King, Steve; Bowen, Jonathan P.

• Format: PDF

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.

---

Dieser Download kann aus rechtlichen Gründen nur mit Rechnungsadresse in A, B, BG, CY, CZ, D, DK, EW, E, FIN, F, GR, HR, H, IRL, I, LT, L, LR, M, NL, PL, P, R, S, SLO, SK ausgeliefert werden.

Produktdetails

• Verlag: Springer Berlin Heidelberg
• Seitenzahl: 554
• Erscheinungstermin: 3. August 2003
• Englisch
• ISBN-13: 9783540448808
• Artikelnr.: 53291240

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.