Wolfram Büttner (auth.), Egon Börger, Michael Butler, Jonathan P. Bowen, Paul Boca (eds.)9783540876021, 3540876022
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.
Table of contents :
Front Matter….Pages –
Complex Hardware Modules Can Now be Made Free of Functional Errors without Sacrificing Productivity….Pages 1-3
The High Road to Formal Validation:….Pages 4-23
Modeling Workflows, Interaction Patterns, Web Services and Business Processes: The ASM-Based Approach….Pages 24-38
Refinement of State-Based Systems: ASMs and Big Commuting Diagrams (Abstract)….Pages 39-41
Model Based Refinement and the Tools of Tomorrow….Pages 42-56
A Concept-Driven Construction of the Mondex Protocol Using Three Refinements….Pages 57-70
A Scenario-Based Validation Language for ASMs….Pages 71-84
Data Flow Analysis and Testing of Abstract State Machines….Pages 85-97
A Verified AsmL Implementation of Belief Revision….Pages 98-111
Direct Support for Model Checking Abstract State Machines by Utilizing Simulation….Pages 112-124
On the Purpose of Event-B Proof Obligations….Pages 125-138
Generating Tests from B Specifications and Test Purposes….Pages 139-152
Combining Scenario- and Model-Based Testing to Ensure POSIX Compliance….Pages 153-166
UseCase-Wise Development: Retrenchment for Event-B….Pages 167-180
Towards Modelling Obligations in Event-B….Pages 181-194
A Practical Single Refinement Method for B….Pages 195-208
The Composition of Event-B Models….Pages 209-222
Reconciling Axiomatic and Model-Based Specifications Reprised….Pages 223-236
A Verifiable Conformance Relationship between Smart Card Applets and B Security Models….Pages 237-250
Modelling Attacker’s Knowledge for Cascade Cryptographic Protocols….Pages 251-264
Using EventB to Create a Virtual Machine Instruction Set Architecture….Pages 265-279
Z2SAL – Building a Model Checker for Z….Pages 280-293
Formal Modeling and Analysis of a Flash Filesystem in Alloy….Pages 294-308
Unit Testing of Z Specifications….Pages 309-322
Autonomous Objects and Bottom-Up Composition in ZOO Applied to a Case Study of Biological Reactivity….Pages 323-336
Integrating Z into Large Projects Tools and Techniques….Pages 337-337
A First Attempt to Express KAOS Refinement Patterns with Event B….Pages 338-338
Verification and Validation of Web Service Composition Using Event B Method….Pages 339-340
Stability of Real-Time Abstract State Machines under Desynchronization….Pages 341-341
XML Database Transformations with Tree Updates….Pages 342-342
Dynamic Resource Configuration & Management for Distributed Information Fusion in Maritime Surveillance….Pages 343-343
UML-B: A Plug-in for the Event-B Tool Set….Pages 344-344
BART: A Tool for Automatic Refinement….Pages 345-345
Model Checking Event-B by Encoding into Alloy….Pages 346-346
A Roadmap for the Rodin Toolset….Pages 347-347
Exploiting the ASM Method for Validation & Verification of Embedded Systems….Pages 348-348
Tool Support for the Circus Refinement Calculus….Pages 349-349
Separation of Z Operations….Pages 350-350
BSmart: A Tool for the Development of Java Card Applications with the B Method….Pages 351-352
From ABZ to Cryptography….Pages 353-353
Using ASM to Achieve Executability within a Family of DSL….Pages 354-354
Using Satisfiability Modulo Theories to Analyze Abstract State Machines (Abstract)….Pages 355-355
Formal Verification of ASM Models Using TLA + ….Pages 356-356
DIR 41 Case Study….Pages 357-357
FDIR Architectures for Autonomous Spacecraft: Specification and Assessment with Event-B….Pages 358-358
Object Modelling in the SystemB Industrial Project….Pages 359-359
Splitting Atoms with Rely/Guarantee Conditions Coupled with Data Reification….Pages 360-377
ABZ2008 VSR-Net Workshop….Pages 378-379
Back Matter….Pages –
Reviews
There are no reviews yet.