From Action Systems to Distributed Systems: The Refinement Approach (Hardcover)

I: MODELING

Modelling Sources for Uncertainty in Environmental Monitoring
Mauno Ronkko
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 Ronkko, and Marina Walden
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
Juri Vain, Leonidas Tsiopoulos, and Pontus Bostrom
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