Abstract State Machines, Alloy, B, TLA, VDM, and Z: 4th International Conference, ABZ 2014, Toulouse, France, June 2-6, 2014. Proceedings

Abstract State Machines, Alloy, B, TLA, VDM, and Z: 4th International Conference, ABZ 2014, Toulouse, France, June 2-6, 2014. Proceedings

Description

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.

Table of contents

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
? RbyAn 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 AspectOriented 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 -

Details

  • Author: Yamine Ait Ameur, Klaus-Dieter Schewe (eds.)
  • Edition: 1
  • Publication Date: 2014
  • Publisher: Springer-Verlag Berlin Heidelberg
  • ISBN-13: 9783662436516, 9783662436523
  • Pages: 348
  • Format: pdf
  • Size: 8.0M
Download Now