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.
Author(s): Cliff B. Jones (auth.), Helen Treharne, Steve King, Martin Henson, Steve Schneider (eds.)
Series: Lecture Notes in Computer Science 3455 : Programming and Software Engineering
Edition: 1
Publisher: Springer-Verlag Berlin Heidelberg
Year: 2005
Language: English
Pages: 496
Tags: Software Engineering; Logics and Meanings of Programs; Mathematical Logic and Formal Languages
Front Matter....Pages -
Specification Before Satisfaction: The Case for Research into Obtaining the Right Specification —Extended Abstract— ....Pages 1-5
Visualising Larger State Spaces in P ro B ....Pages 6-23
Non-atomic Refinement in Z and CSP....Pages 24-44
Process Refinement in B....Pages 45-64
CZT: A Framework for Z Tools....Pages 65-84
Model Checking Z Specifications Using SAL....Pages 85-103
Proving Properties of Stateflow Models Using ISO Standard Z and CADiZ....Pages 104-123
A Stepwise Development of the Peterson’s Mutual Exclusion Algorithm Using B Abstract Systems....Pages 124-141
An Extension of Event B for Developing Grid Systems....Pages 142-161
The Challenge of Probabilistic Event B—Extended Abstract— ....Pages 162-171
Requirements as Conjectures: Intuitive DVD Menu Navigation....Pages 172-186
A Prospective-Value Semantics for the GSL....Pages 187-202
Retrenchment and the B-Toolkit....Pages 203-221
Refinement and Reachability in Event_B....Pages 222-241
A Rigorous Foundation for Pattern-Based Design Models....Pages 242-261
An Object-Oriented Structuring for Z Based on Views....Pages 262-278
Component Reuse in B Using ACL2....Pages 279-298
GeneSyst : A Tool to Reason About Behavioral Aspects of B Event Specifications. Application to Security Properties....Pages 299-318
Formal Verification of a Type Flaw Attack on a Security Protocol Using Object-Z....Pages 319-333
Using B as a High Level Programming Language in an Industrial Project: Roissy VAL....Pages 334-354
Development via Refinement in Probabilistic B — Foundation and Case Study....Pages 355-373
Formal Program Development with Approximations....Pages 374-392
Practical Data Refinement for the Z Schema Calculus....Pages 393-413
Slicing Object-Z Specifications for Verification....Pages 414-433
Checking JML Specifications with B Machines....Pages 434-453
Including Design Guidelines in the Formal Specification of Interfaces in Z....Pages 454-471
Some Guidelines for Formal Development of Web-Based Applications in B-Method....Pages 472-492
Back Matter....Pages -
