Abstract State Machines, B and Z: First International Conference, ABZ 2008, London, UK, September 16-18, 2008. Proceedings (Lecture Notes in Computer Science, 5238)

First International Conference, ABZ 2008, London, UK, September 16-18, 2008. Proceedings (Lecture Notes in Computer Science) 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. 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 - Egon Börger ... [et Al.] (eds.). Includes Bibliographical References And Index.