Abstract State Machines, Alloy, B, TLA, VDM, and Z : 5th International Conference, ABZ 2016, Linz, Austria, May 23-27, 2016, Proceedings / edited by Michael Butler, Klaus-Dieter Schewe, Atif Mashkoor, Miklos Biro.

Format:

Book

Contributor:

Butler, Michael (Editor), editor.

Schewe, Klaus-Dieter, editor.

Mashkoor, Atif, editor.

Biro, Mikloš, editor.

SpringerLink (Online service)

Series:

Computer Science (Springer-11645)

LNCS sublibrary. Theoretical computer science and general issues ; SL 1, 9675.

Theoretical Computer Science and General Issues ; 9675

Language:

English

Subjects (All):

Logic, Symbolic and mathematical.

Computer logic.

Computers.

Software engineering.

Programming languages (Electronic computers).

Mathematical Logic and Formal Languages.

Logics and Meanings of Programs.

Computation by Abstract Devices.

Software Engineering.

Programming Languages, Compilers, Interpreters.

Local Subjects:

Mathematical Logic and Formal Languages.

Logics and Meanings of Programs.

Computation by Abstract Devices.

Software Engineering.

Programming Languages, Compilers, Interpreters.

Physical Description:

1 online resource (XXI, 426 pages) : 143 illustrations.

Edition:

First edition 2016.

Contained In:

Springer eBooks

Place of Publication:

Cham : Springer International Publishing : Imprint: Springer, 2016.

System Details:

text file PDF

Summary:

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.

Contents:

Modeling Distributed Algorithms by Abstract State Machines Compared to Petri Nets

A Universal Control Construct for Abstract State Machines

Encoding TLA+ into Many-Sorted First-Order Logic

Proving Determinacy of PharOS in TLA+

A Rigorous Correctness Proof for Pastry

Enabling Analysis for B and Event-B

A Compact Encoding of Sequential ASMs in Event-B

Proof Assisted Symbolic Model Checking for B and Event-B

On Component-based Reuse for Event-B

Using B and ProB for Data Validation Projects

Generating Event-B Specifications from Algorithm Descriptions

Formal Proofs of Termination Detection for Local Computations by Refinement-Based Compositions

How to Select the Suitable Formal Method for an Industrial Application: A Survey

Unified Syntax for Abstract State Machines

A Relational Encoding for a Clash-Free Subset of ASMs

Towards an ASM Thesis for Reflective Sequential Algorithms

A Model-based Transformation Approach to Reuse and Retarget CASM Specifications

Modeling a Discrete Wet-Dry Algorithm for Hurricane Storm Surge in Alloy

`The Tinker' for Rodin

A Graphical Tool for Event Refinement Structures in Event-B

Rodin Platform Why3 plug-in

Semi-Automated Design Space Exploration for Formal Modelling

Handling Continuous Functions in Hybrid Systems Reconfigurations: A Formal Event-B Development

UC-B: Use Case Modelling with Event-B

Interactive Model Repair by Synthesis

SysML2B: Automatic Tool for B Project Graphical Architecture Design using SysML

Mechanized Refinement of Communication Models with TLA+

A Super Industrial Application of PSGraph

The Hemodialysis Machine Case Study

How to Assure Correctness and Safety of Medical Software: The Hemodialysis Machine Case Study

Validating the Requirements and Design of a Hemodialysis Machine Using iUML-B, BMotionStudio, and Co-simulation

Hemodialysis Machine in Hybrid Event-B

Modeling a Hemodialysis Machine using Algebraic State-Transition Diagrams and B-like Methods

Modelling the Haemodialysis Machine with Circus.

Other Format:

Printed edition:

ISBN:

978-3-319-33600-8

9783319336008

Access Restriction:

Restricted for use by site license.