ZB 2005: Formal Specification and Development in Z and BZB 2005：Z与B的形式规格说明与开发/会议录

This book constitutes the refereed proceedings of the 4th International Conference of Z and B users, ZB 2005, held in Guildford, UK in April 2005.
The 25 revised full papers presented together with extended abstracts of 2 invited papers were carefully reviewed and selected for inclusion in the book. The papers document the recent advances for the Z formal specification notation and for the B method, ranging from foundational, theoretical, and methodological issues to advanced applications, tools, and case studies.

The LNCS series reports state-of-the-art results in computer science research，development，and education，at a high level and in both printed and electronic form. Enjoying tight cooperation with the R&D community，with numerous individuals，as well as with prestigious organizations and societies，LNCS has grown into the most comprehensive computer science research forum available.
The scope of LNCS，including its subseries LNAI，spans the whole range of computer science and information technology including interdisciplinary topics in a variety of application fields. The type of material published traditionally includes.
—proceedings （published in time for the respective conference）
—post-proceedings （consisting of thoroughly revised final full papers）
—research monographs（which may be based on outstanding PhD work，research projects，technical reports，etc.）

Specification Before Satisfaction: The Case for Research into Obtaining
the Right Specification (Extended Abstract)
Visualising Larger State Spaces in PROB
Non-atomic Refinement in Z and CSP
Process Refinement in B
CZT: A Framework for Z Tools
Model Checking Z Specifications Using SAL
Proving Properties of Stateflow Models Using ISO Standard Z and CADIZ
A Stepwise Development of the Peterson's Mutual Exclusion Algorithm Using B Abstract Systems
An Extension of Event B for Developing Grid Systems
The Challenge of Probabilistic Event B (Extended Abstract)
Requirements as Conjectures: Intuitive DVD Menu Navigation
A Prospective-Value Semantics for the GSL
Retrenchment and the B-Toolkit
Refinement and Reachability in Event_B
A Rigorous Foundation for Pattern-Based Design Models
An Object-Oriented Structuring for Z Based on Views
Component Reuse in B Using ACL2
GeneSyst: A Tool to Reason About Behavioral Aspects of B Event
Formal Verification of a Type Flaw Attack on a Security Protocol Using Object-Z
Using B as a High Level Programming Language in an Industrial Project: Roissy VAL
Development via Refinement in Probabilistic B -- Foundation and Case Study
Formal Program Development with Approximations
Practical Data Refinement for the Z Schema Calculus
Slicing Object-Z Specifications for Verification
Checking JML Specifications with B Machines
Including Design Guidelines in the Formal Specification of Interfaces in Z
Some Guidelines for Formal Development of Web-Based Applicatins in B-Method
Author Index