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

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.

Produktdetails

• Lecture Notes in Computer Science 2651
• Verlag: Springer / Springer Berlin Heidelberg / Springer, Berlin
• Artikelnr. des Verlages: 978-3-540-40253-4
• 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.