Formal specification and development in Z and B

InhaltsverzeichnisSpecification 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.