Abstract State Machines, B and Z

This book constitutes the refereed proceedings of the First International Conference of Abstract State Machines, B and Z, ABZ 2008, held in London, UK, in September 2008. The conference simultaneously incorporated the 15th International ASM Workshop, the 17th International Conference of Z Users and the 8th International Conference on the B Method. The 44 revised full papers presented together with 4 invited contributions were carefully reviewed and selected from numerous submissions. The conference fosters the cross-fertilization of three rigorous methods for the design and analysis of hardware and software systems - both in academia and industry - namely Abstract State Machines, B, and Z. Covering a wide range of research spanning from theoretical and methodological foundations to tool support and practical applications, the contributions are organized in topical sections on abstract state machines, B papers, Z papers, ABZ short papers, and the papers of the Verified Software Repository Network (VSR-net) workshop.

1. ABZ Invited Talks. - Complex Hardware Modules Can Now be Made Free of Functional Errors without Sacrificing Productivity. - The High Road to Formal Validation:. - Modeling Workflows, Interaction Patterns, Web Services and Business Processes: The ASM-Based Approach. - Refinement of State-Based Systems: ASMs and Big Commuting Diagrams (Abstract). - 2. ASM Papers. - Model Based Refinement and the Tools of Tomorrow. - A Concept-Driven Construction of the Mondex Protocol Using Three Refinements. - A Scenario-Based Validation Language for ASMs. - Data Flow Analysis and Testing of Abstract State Machines. - A Verified AsmL Implementation of Belief Revision. - Direct Support for Model Checking Abstract State Machines by Utilizing Simulation. - 3. B Papers. - On the Purpose of Event-B Proof Obligations. - Generating Tests from B Specifications and Test Purposes. - Combining Scenario- and Model-Based Testing to Ensure POSIX Compliance. - UseCase-Wise Development: Retrenchment for Event-B. - Towards Modelling Obligations in Event-B. - A Practical Single Refinement Method for B. - The Composition of Event-B Models. - Reconciling Axiomatic and Model-Based Specifications Reprised. - A Verifiable Conformance Relationship between Smart Card Applets and B Security Models. - Modelling Attacker s Knowledge for Cascade Cryptographic Protocols. - Using EventB to Create a Virtual Machine Instruction Set Architecture. - 4. Z Papers. - Z2SAL - Building a Model Checker for Z. - Formal Modeling and Analysis of a Flash Filesystem in Alloy. - Unit Testing of Z Specifications. - Autonomous Objects and Bottom-Up Composition in ZOO Applied to a Case Study of Biological Reactivity. - 5. ABZ Short Papers. - Integrating Z into Large Projects Tools and Techniques. - A First Attempt to Express KAOS Refinement Patterns with EventB. - Verification and Validation of Web Service Composition Using Event B Method. - Stability of Real-Time Abstract State Machines under Desynchronization. - XML Database Transformations with Tree Updates. - Dynamic Resource Configuration & Management for Distributed Information Fusion in Maritime Surveillance. - UML-B: A Plug-in for the Event-B Tool Set. - BART: A Tool for Automatic Refinement. - Model Checking Event-B by Encoding into Alloy. - A Roadmap for the Rodin Toolset. - Exploiting the ASM Method for Validation & Verification of Embedded Systems. - Tool Support for the Circus Refinement Calculus. - Separation of Z Operations. - BSmart: A Tool for the Development of Java Card Applications with the B Method. - From ABZ to Cryptography. - Using ASM to Achieve Executability within a Family of DSL. - Using Satisfiability Modulo Theories to Analyze Abstract State Machines (Abstract). - Formal Verification of ASM Models Using TLA? +? . - DIR 41 Case Study. - FDIR Architectures for Autonomous Spacecraft: Specification and Assessment with Event-B. - Object Modelling in the SystemB Industrial Project. - 6. VSR Day. - Splitting Atoms with Rely/Guarantee Conditions Coupled with Data Reification. - ABZ2008 VSR-Net Workshop.