This book constitutes the refereed proceedings of the First International Conference of B and Z Users, ZB 2000, held in York, UK in August/September 2000.
The 25 revised full papers presented together with four invited contributions were carefully reviewed and selected for inclusion in the book. The book documents the recent advances for the Z formal specification notion and for the B method; the full scope, ranging from foundational and theoretical issues to advanced applications, tools, and case studies, is covered.
Author(s): Mike Spivey (auth.)
Series: Lecture Notes in Computer Science 1878
Edition: 1
Publisher: Springer-Verlag Berlin Heidelberg
Year: 2000
Language: English
Pages: 510
Tags: Software Engineering; Logics and Meanings of Programs; Programming Techniques; Mathematical Logic and Formal Languages
Meeting the Challenge of Object-Oriented Programming....Pages 1-1
A Formal Mapping between UML Models and Object-Z Specifications....Pages 2-21
A Generic Process to Refine a B Specification into a Relational Database Implementation....Pages 22-41
Recursive Schema Definitions in Object-Z....Pages 42-58
On Mutually Recursive Free Types in Z....Pages 59-74
Reasoning Inductively about Z Specifications via Unification....Pages 75-94
Reconciling Axiomatic and Model-Based Specifications Using the B Method....Pages 95-106
Compositional Structuring in the B-Method: A Logical Viewpoint of the Static Context....Pages 107-126
Automatic Construction of Validated B Components from Structured Developments....Pages 127-147
Playing with Abstraction and Refinement for Managing Features Interactions....Pages 148-167
A Formal Architecture for the 3APL Agent Programming Language....Pages 168-187
How to Drive a B Machine....Pages 188-208
Deriving Software Specifications from Event Based Models....Pages 209-229
Reformulate Dynamic Properties during B Refinement and Forget Variants and Loop Invariants....Pages 230-249
Type-Constrained Generics for Z....Pages 250-263
Typechecking Z....Pages 264-285
Guards, Preconditions, and Refinement in Z....Pages 286-303
Retrenchment, Refinement, and Simulation....Pages 304-323
Performing Algorithmic Refinement before Data Refinement in B....Pages 324-343
Program Development and Specification Refinement in the Schema Calculus....Pages 344-362
Are Smart Cards the Ideal Domain for Applying Formal Methods....Pages 363-373
Formal Methods for Industrial Products....Pages 374-393
An Execution Architecture for GSL....Pages 394-413
A Computation Model for Z Based on Concurrent Constraint Resolution....Pages 414-432
Analysis of Compiled Code: A Prototype Formal Model....Pages 433-449
Zzzzzzzzzzzzzzzzzzzzzzzzzz....Pages 450-450
Segregation with Communication....Pages 451-470
Closure Induction in a Z-Like Language....Pages 471-490
Fuzzy Concepts and Formal Methods: A Fuzzy Logic Toolkit for Z....Pages 491-510
