Abstract State Machines, Alloy, B, TLA, VDM, and Z: 5th International Conference, ABZ 2016, Linz, Austria, May 23-27, 2016, Proceedings

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