Abstract State Machines, B and Z: First International Conference, ABZ 2008, London, UK, September 16-18, 2008. ProceedingsEgon Börger 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. |
Contents
Complex Hardware Modules Can Now be Made Free of Functional Errors without Sacrificing Productivity | 1 |
Model Checking HighLevel Versus LowLevel Specifications | 4 |
The ASMBased Approach | 24 |
ASMs and Big Commuting Diagrams | 39 |
Model Based Refinement and the Tools of Tomorrow | 42 |
A ConceptDriven Construction of the Mondex Protocol Using Three Refinements | 57 |
A ScenarioBased Validation Language for ASMs | 71 |
Data Flow Analysis and Testing of Abstract State Machines | 85 |
Integrating Z into Large Projects Tools and Techniques | 337 |
A First Attempt to Express KAOS Refinement Patterns with Event B | 338 |
Verification and Validation of Web Service Composition Using Event B Method | 339 |
Stability of RealTime Abstract State Machines under Desynchronization | 341 |
XML Database Transformations with Tree Updates | 342 |
Dynamic Resource Configuration Management for Distributed Information Fusion in Maritime Surveillance | 343 |
A Plugin for the EventB Tool Set | 344 |
A Tool for Automatic Refinement | 345 |
A Verified AsmL Implementation of Belief Revision | 98 |
Direct Support for Model Checking Abstract State Machines by Utilizing Simulation | 112 |
On the Purpose of EventB Proof Obligations | 125 |
Generating Tests from B Specifications and Test Purposes | 139 |
Combining Scenario and ModelBased Testing to Ensure POSIX Compliance | 153 |
Retrenchment for EventB | 167 |
Towards Modelling Obligations in EventB | 181 |
A Practical Single Refinement Method for B | 195 |
The Composition of EventB Models | 209 |
Reconciling Axiomatic and ModelBased Specifications Reprised | 223 |
A Verifiable Conformance Relationship between Smart Card Applets and B Security Models | 237 |
Modelling Attackers Knowledge for Cascade Cryptographic Protocols | 251 |
Using EventB to Create a Virtual Machine Instruction Set Architecture | 265 |
Z2SAL Building a Model Checker for Z | 280 |
Formal Modeling and Analysis of a Flash Filesystem in Alloy | 294 |
Unit Testing of Z Specifications | 309 |
Autonomous Objects and BottomUp Composition in ZOO Applied to a Case Study of Biological Reactivity | 323 |
Model Checking EventB by Encoding into Alloy | 346 |
A Roadmap for the Rodin Toolset | 347 |
Exploiting the ASM Method for Validation Verification of Embedded Systems | 348 |
Tool Support for the Circus Refinement Calculus | 349 |
Separation of Z Operations | 350 |
A Tool for the Development of Java Card Applications with the B Method | 351 |
From ABZ to Cryptography | 353 |
Using ASM to Achieve Executability within a Family of DSL | 354 |
Using Satisfiability Modulo Theories to Analyze Abstract State Machines | 355 |
Formal Verification of ASM Models Using TLA+ | 356 |
DIR 41 Case Study How EventB Can Improve an Industrial System Specification | 357 |
Specification and Assessment with EventB | 358 |
Object Modelling in the SystemB Industrial Project | 359 |
Splitting Atoms with RelyGuarantee Conditions Coupled with Data Reification | 360 |
ABZ2008 VSRNet Workshop | 378 |
| 380 | |