Abstract State Machines, B and Z

1. Front Matter

   PDF

2. Chapter 1. ABZ Invited Talks

   1. Complex Hardware Modules Can Now be Made Free of Functional Errors without Sacrificing Productivity

      • Wolfram Büttner

      Pages 1-3

   2. The High Road to Formal Validation:

      • Michael Leuschel

      Pages 4-23

   3. Modeling Workflows, Interaction Patterns, Web Services and Business Processes: The ASM-Based Approach

      • Egon Börger, Bernhard Thalheim

      Pages 24-38

   4. Refinement of State-Based Systems: ASMs and Big Commuting Diagrams (Abstract)

      • Gerhard Schellhorn

      Pages 39-41

3. Chapter 2. ASM Papers

   1. Model Based Refinement and the Tools of Tomorrow

      • Richard Banach

      Pages 42-56

   2. A Concept-Driven Construction of the Mondex Protocol Using Three Refinements

      • Gerhard Schellhorn, Richard Banach

      Pages 57-70

   3. A Scenario-Based Validation Language for ASMs

      • Alessandro Carioni, Angelo Gargantini, Elvinia Riccobene, Patrizia Scandurra

      Pages 71-84

   4. Data Flow Analysis and Testing of Abstract State Machines

      • Alessandra Cavarra

      Pages 85-97

   5. A Verified AsmL Implementation of Belief Revision

      • Christoph Beierle, Gabriele Kern-Isberner

      Pages 98-111

   6. Direct Support for Model Checking Abstract State Machines by Utilizing Simulation

      • Jörg Beckers, Daniel Klünder, Stefan Kowalewski, Bastian Schlich

      Pages 112-124

4. Chapter 3. B Papers

   1. On the Purpose of Event-B Proof Obligations

      • Stefan Hallerstede

      Pages 125-138

   2. Generating Tests from B Specifications and Test Purposes

      • Jacques Julliand, Pierre-Alain Masson, Régis Tissot

      Pages 139-152

   3. Combining Scenario- and Model-Based Testing to Ensure POSIX Compliance

      • Frédéric Dadeau, Adrien De Kermadec, Régis Tissot

      Pages 153-166

   4. UseCase-Wise Development: Retrenchment for Event-B

      • Richard Banach

      Pages 167-180

   5. Towards Modelling Obligations in Event-B

      • Juan Bicarregui, Alvaro Arenas, Benjamin Aziz, Philippe Massonet, Christophe Ponsard

      Pages 181-194

   6. A Practical Single Refinement Method for B

      • Steve Dunne, Stacey Conroy

      Pages 195-208

   7. The Composition of Event-B Models

      • Michael Poppleton

      Pages 209-222

   8. Reconciling Axiomatic and Model-Based Specifications Reprised

      • Ken Robinson

      Pages 223-236

   9. A Verifiable Conformance Relationship between Smart Card Applets and B Security Models

      • Frédéric Dadeau, Julien Lamboley, Thierry Moutet, Marie-Laure Potet

      Pages 237-250

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.

• B method
• abstract state machines
• access control
• automatic verification
• complex systems
• cryptography
• design
• design process
• distributed systems
• dynamically configurable systems
• event-B
• formal methods
• formal software development
• formal specification

Policies and ethics