Abstract State Machines, B and Z: First International Conference, ABZ 2008, London, UK, September 16-18, 2008. Proceedings

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 -