Librería Portfolio

Features

Explores the impact of the Action Systems formal method on computer science research
Covers the historical background of formal methods research, as well as current research on action systems
Describes the transition from the strong theory of refinement to a methodology that can be applied in practice, with tool support
Presents contributions form renowned researchers
Examines industrial applications of these methods
Summary

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 Ruks?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