Formal specification and development in Z and B

InhaltsverzeichnisAlloy: 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.