ZB 2005: Formal Specification and Development in Z and B (eBook, PDF)

4th International Conference of B and Z Users, Guildford, UK, April 13-15, 2005, Proceedings
Redaktion: Treharne, Helen; Schneider, Steve; Henson, Martin; King, Steve

• Format: PDF

Produktdetails

• Verlag: Springer Berlin Heidelberg
• Seitenzahl: 496
• Erscheinungstermin: 25. April 2005
• Englisch
• ISBN-13: 9783540320074
• Artikelnr.: 44131172

Autorenporträt

Helen Treharne, University of Surrey, Guildford, UK / Steve King, University of York, UK / Martin Henson, University of Essex, Colchester, UK / Steve Schneider, University of Surrey, Guildford, UK

Inhaltsangabe

Specification Before Satisfaction: The Case for Research into Obtaining the Right Specification -Extended Abstract-.- Visualising Larger State Spaces in Pro B.- 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 Specifications. Application to Security Properties.- 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 Applications in B-Method.