Overview

Full Product Details

Author:   Michael Butler ,  Klaus-Dieter Schewe ,  Atif Mashkoor ,  Miklos Biro
Publisher:   Springer International Publishing AG
Imprint:   Springer International Publishing AG
Edition:   1st ed. 2016
Volume:   9675
Dimensions:   Width: 15.50cm , Height: 2.30cm , Length: 23.50cm
Weight:   0.682kg
ISBN:  

9783319335995

ISBN 10:   3319335995
Pages:   426
Publication Date:   11 May 2016
Audience:   Professional and scholarly ,  Professional & Vocational
Format:   Paperback
Publisher's Status:   Active
Availability:   Manufactured on demand  
We will order this item for you from a manufactured on demand supplier.

Table of 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.

Reviews

Author Information

Tab Content 6

Author Website:  

Customer Reviews

Recent Reviews

No review item found!

Add your own review!

Countries Available

All regions