From Action Systems to Distributed Systems: The Refinement Approach, 1st Edition (Hardback) book cover

From Action Systems to Distributed Systems

The Refinement Approach, 1st Edition

Edited by Luigia Petre, Emil Sekerinski

Chapman and Hall/CRC

284 pages | 80 B/W Illus.

Purchasing Options:$ = USD
Hardback: 9781498701587
pub: 2016-04-27
SAVE ~$39.00
$195.00
$156.00
x
eBook (VitalSource) : 9780429075681
pub: 2016-04-27
from $28.98


FREE Standard Shipping!

Description

Formal methods traditionally address the question of transforming software engineering into a mature engineering discipline. This essentially refers to trusting that the software-intensive systems that form our society’s infrastructures are behaving according to their specifications. More recently, formal methods are also used to understand properties and evolution laws of existing complex and adaptive systems—man-made such as smart electrical grids or natural ones such as biological networks.

A tribute to Professor Kaisa Sere’s contributions to the field of computer science, From Action Systems to Distributed Systems: The Refinement Approach is the first book to address the impact of refinement through a multitude of formal methods ranging from Action Systems to numerous related approaches in computer science research. It presents a state-of-the-art review on the themes of distributed systems and refinement.

A fundamental part of Kaisa Sere’s research consisted of developing Action Systems, a formalism for modeling, analysing, and constructing distributed systems. Within the design of distributed systems, Kaisa Sere’s main research focus was on refinement-based approaches to the construction of systems ranging from pure software to hardware and digital circuits.

Presenting scientific contributions from renowned researchers around the world, this edited book consists of five sections: Modeling, Analysis, Proof, Refinement, and Applications. Each chapter has been thoroughly reviewed by experts in the field. The book covers both traditional aspects in formal methods research, as well as current and innovative research directions. It describes the transition from the strong theory of refinement to a methodology that can be applied in practice, with tool support.

Examining industrial applications of the methods discussed, this book is a suitable resource for graduate students, researchers, and practitioners interested in using formal methods to develop distributed systems of quality.

Table of Contents

I: MODELING

Modelling Sources for Uncertainty in Environmental Monitoring

Mauno Rönkkö

Introduction

Hybrid Action Systems

Environmental Monitoring

Case Study: Monitoring Room Temperature

Conclusion

Mandatory and Potential Choice: Comparing Event-B and STAIRS

Atle Refsdal, Ragnhild Kobro Runde, and Ketil Stølen

Introduction

Kinds of Choice

Comparing Event-B and STAIRS at the Syntactic Level

Interaction-Obligations versus Failure-Divergences

Conclusion

Modelling and Refining Hybrid Systems in Event-B and Rodin

Michael Butler, Jean-Raymond Abrial, and Richard Banach

Introduction

Reals and Continuous Functions

Modelling a Continuous Control Goal

Distinguishing Modes

Modelling the Control Strategy

Merging Big and Small Step Variables

Derivatives

Concluding

II: ANALYSIS

Modelling and Analysis of Component Faults and Reliability

Thibaut Le Guilly, Petur Olsen, Anders P. Ravn, and Arne Skou

Introduction

A Development and Analysis Process

Example

Discussion, Conclusion, Related and Further Work

Verifiable Programming of Object-Oriented and Distributed Systems

Olaf Owe

Introduction

Basic Programming Constructs

Class Invariants

Inheritance

Local Reasoning

Discussion of Future-Related Mechanisms

Conclusion

A Contract-Based Approach to Ensuring Component Interoperability in Event-B

Linas Laibinis and Elena Troubitsyna

Introduction

Background: Event-B

From Event-B Modelling to Contracts

Example: an Auction System

Conclusions

III: PROOF

Meeting Deadlines, Elastically

Einar Broch Johnsen, Ka I Pun, Martin Steffen, S. Lizeth Tapia Tarifa, and Ingrid Chieh Yu

Introduction

Service Contracts as Interfaces

A Kernel Language for Virtualized Computing

Example: A Photo Printing Shop

Proof System

Related Work

Discussion

Event-B and Linear Temporal Logic

Steve Schneider, Helen Treharne, and David M. Williams

Introduction

Event-B

LTL Notation

Preserving LTL Properties in Event-B Refinement Chains

Discussion and Related Work

Conclusion

A Provably Correct Resilience Mediator Pattern

Mats Neovius, Mauno Rönkkö, and Marina Waldén

Introduction

Provably Correct Stepwise Development with Action Systems

Resilience Mediator

Formal Development of the Resilience Mediator Pattern

Discussion and Conclusion

IV: REFINEMENT

Relational Concurrent Refinement - Partial and Total Frameworks

John Derrick and Eerke Boiten

Introduction

Models of Refinement

Using a Partial Framework to Embed Concurrent Refinement Relations

A Total Relational Framework

A General Framework for Simulations - Process Data Types

Conclusions

Refinement of Behavioural Models for Variability Description

Alessandro Fantechi and Stefania Gnesi

Introduction

Running Example and Background

Behavioural Models and Variability

A Comparison on the Expressiveness11.5 Conclusions

Acknowledgments

Integrating Refinement-Based Methods for Developing Timed Systems

Jüri Vain, Leonidas Tsiopoulos, and Pontus Boström

Introduction

Related Work

Preliminaries

Mapping from Event-B Models to UPTA

IEEE 1394 Case Study

Refinement of Timed Systems

Conclusion and Future Work

V: APPLICATIONS

Action Systems for Pharmacokinetic Modeling

M.M. Bonsangue, M. Helvensteijn, J.N. Kok, and N. Kokash

Introduction

Actions and Action Systems

Pharmacokinetic Modeling

Conclusions and Future Work

Quantitative Model Refinement in Four Different Frameworks

Diana-Elena Gratie, Bogdan Iancu, Sepinoud Azimi, and Ion Petre

Introduction

Quantitative Model Refinement

Case Study: the Heat Shock Response (HSR)

Quantitative Refinement for ODE Models

Quantitative Refinement for Rule-Based Models

Quantitative Refinement for Petri Net Models

Quantitative Refinement for PRISM Models

Discussion

Developing and Verifying User Interface Requirements for Infusion Pumps: A Refinement Approach

Rimvydas Rukš˙enas, Paolo Masci, and Paul Curzon

Introduction

Sample User Interface Requirements from FDA

Background

The Requirement Hierarchies

Verification of Concrete Interfaces

Conclusions

Self-Assembling Interactive Modules: A Research Programme

Gheorghe Stefanescu

Tiling - a Brief Introduction

Two-Dimensional Languages: Local vs. Global Glueing Constraints

Structural Characterisation for Self-Assembling Tiles

Interactive Programs

Conclusions

Bibliography

Subject Categories

BISAC Subject Codes/Headings:
COM012040
COMPUTERS / Programming / Games
COM031000
COMPUTERS / Information Theory
COM051230
COMPUTERS / Software Development & Engineering / General
MAT000000
MATHEMATICS / General