Abstract State Machines, Alloy, B, TLA, VDM, and Z: 4th International Conference, ABZ 2014, Toulouse, France, June 2-6, 2014. Proceedings (Lecture Notes in Computer Science, 8477)

This book constitutes the thoroughly refereed proceedings of the 4th International Conference on Abstract State Machines, B, TLA, VDM, and Z, which took place in Toulouse, France, in June 2014. The 13 full papers presented together with 3 invited talks and 19 short papers were carefully reviewed and selected from 81 submissions. The ABZ conference series is dedicated to the cross-fertilization of six related state-based and machine-based formal methods: Abstract State Machines (ASM), Alloy, B, TLA, VDM, and Z. They share a common conceptual foundation and are widely used in both academia and industry for the design and analysis of hardware and software systems. The main goal of this conference series is to contribute to the integration of these formal methods, clarifying their commonalities and differences to better understand how to combine different approaches for accomplishing the various tasks in modeling, experimental validation and mathematical verification of reliable high-quality hardware/software systems Front Matter....Pages - The Rodin Platform Has Turned Ten....Pages 1-8 Development of a Verified Flash File System....Pages 9-24 Why Amazon Chose TLA + ....Pages 25-39 Translating B to TLA + for Validation with TLC....Pages 40-55 α Rby—An Embedding of Alloy in Ruby....Pages 56-71 MAZE: An Extension of Object-Z for Multi-Agent Systems....Pages 72-85 Quasi-Lexicographic Convergence....Pages 86-100 Towards B as a High-Level Constraint Modelling Language....Pages 101-116 Analysis of Self-⋆ and P2P Systems Using Refinement....Pages 117-123 B Formal Validation of ERTMS/ETCS Railway Operating Rules....Pages 124-129 Modelling Energy Consumption in Embedded Systems with VDM-RT....Pages 130-135 Sealed Containers in Z....Pages 136-141 Specifying Transaction Control to Serialize Concurrent Program Executions....Pages 142-157 Distributed Situation Analysis....Pages 158-173 Introducing Aspect–Oriented Specification for Abstract State Machines....Pages 174-187 Modular Refinement for Submachines of ASMs....Pages 188-203 Towards ASM-Based Formal Specification of Self-Adaptive Systems....Pages 204-209 Distributed ASM - Pitfalls and Solutions....Pages 210-215 WebASM: An Abstract State Machine Execution Environment for the Web....Pages 216-221 Formal System Modelling Using Abstract Data Types in Event-B....Pages 222-237 Formal Derivation of Distributed MapReduce....Pages 238-254 Validating the RBAC ANSI 2012 Standard Using B....Pages 255-270 Invariant Guided System Decomposition....Pages 271-276 Understanding and Planning Event-B Refinement through Primitive Rationales....Pages 277-283 Templates for Event-B Code Generation....Pages 284-289 The BWare Project: Building a Proof Platform for the Automated Verification of B Proof Obligations....Pages 290-293 Tuning the Alt-Ergo SMT Solver for B Proof Obligations....Pages 294-297 Fixed-Point Arithmetic Modeled in B Software Using Reals....Pages 298-302 Bounded Model Checking of Temporal Formulas with Alloy....Pages 303-308 Formal Verification of OS Security Model with Alloy and Event-B....Pages 309-313 Detecting Network Policy Conflicts Using Alloy....Pages 314-317 Staged Evaluation of Partial Instances in a Relational Model Finder....Pages 318-323 Domain-Specific Visualization of Alloy Instances....Pages 324-327 Optimizing Alloy for Multi-objective Software Product Line Configuration....Pages 328-333 Back Matter....Pages -