ZB 2003: Formal Specification and Development in Z and B

Inhaltsverzeichnis

• 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.