Abstract State Machines, Alloy, B, TLA, VDM, and Z: 5th International Conference, ABZ 2016, Linz, Austria, May 23-27, 2016, Proceedings (Lecture Notes in Computer Science Book 9675)

The use of general descriptive names, registered names, trademarks, service marks, etc. in this publication does not imply, even in the absence of a specific statement, that such names are exempt from the relevant protective laws and regulations and therefore free for general use. The publisher, the authors and the editors are safe to assume that the advice and information in this book are believed to be true and accurate at the date of publication. Neither the publisher nor the authors or the editors give a warranty, express or implied, with respect to the material contained herein or for any errors or omissions that may have been made. Front Matter....Pages I-XXI Front Matter....Pages 1-1 Modeling Distributed Algorithms by Abstract State Machines Compared to Petri Nets....Pages 3-34 Front Matter....Pages 35-35 A Universal Control Construct for Abstract State Machines....Pages 37-53 Proving Determinacy of the PharOS Real-Time Operating System....Pages 54-69 A Rigorous Correctness Proof for Pastry....Pages 70-85 Enabling Analysis for Event-B....Pages 86-101 A Compact Encoding of Sequential ASMs in Event-B....Pages 102-118 Proof Assisted Symbolic Model Checking for B and Event-B....Pages 119-134 On Component-Based Reuse for Event-B....Pages 135-150 Using B and ProB for Data Validation Projects....Pages 151-166 Generating Event-B Specifications from Algorithm Descriptions....Pages 167-182 Formal Proofs of Termination Detection for Local Computations by Refinement-Based Compositions....Pages 183-197 How to Select the Suitable Formal Method for an Industrial Application: A Survey....Pages 198-212 Front Matter....Pages 213-228 Unified Syntax for Abstract State Machines....Pages 229-229 A Relational Encoding for a Clash-Free Subset of ASMs....Pages 231-236 Towards an ASM Thesis for Reflective Sequential Algorithms....Pages 237-243 A Model-Based Transformation Approach to Reuse and Retarget CASM Specifications....Pages 244-249 Modeling a Discrete Wet-Dry Algorithm for Hurricane Storm Surge in Alloy....Pages 250-255 ‘The Tinker’ for Rodin....Pages 256-261 A Graphical Tool for Event Refinement Structures in Event-B....Pages 262-268 Front Matter....Pages 269-274 Rodin Platform Why3 Plug-In....Pages 229-229 Semi-Automated Design Space Exploration for Formal Modelling....Pages 275-281 Handling Continuous Functions in Hybrid Systems Reconfigurations: A Formal Event-B Development....Pages 282-289 UC-B: Use Case Modelling with Event-B....Pages 290-296 Interactive Model Repair by Synthesis....Pages 297-302 SysML2B: Automatic Tool for B Project Graphical Architecture Design Using SysML....Pages 303-307 A Super Industrial Application of PSGraph....Pages 308-311 Front Matter....Pages 312-318 The Hemodialysis Machine Case Study....Pages 319-325 How to Assure Correctness and Safety of Medical Software: The Hemodialysis Machine Case Study ....Pages 327-327 Validating the Requirements and Design of a Hemodialysis Machine Using iUML-B, BMotion Studio, and Co-Simulation....Pages 329-343 Hemodialysis Machine in Hybrid Event-B....Pages 344-359 Modelling a Hemodialysis Machine Using Algebraic State-Transition Diagrams and B-like Methods....Pages 360-375 Back Matter....Pages 376-393 ....Pages 394-408 This book constitutes the refereed proceedings of the 5th International Conference on Abstract State Machines, Alloy, B, TLA, VDM, and Z, ABZ 2016, held in Linz, Austria, in May 2016. The 17 full and 15 short papers presented in this volume were carefully reviewed and selected from 61 submissions. They record the latest research developments in state-based formal methods Abstract State Machines, Alloy, B, Circus, Event-B, TLS+, VDM and Z.