Integrating Event-B Modelling and Discrete-Event Simulation to Analyse Resilience of Data Stores in the Cloud

A4 Conference proceedings

Internal Authors/Editors

Publication Details

List of Authors: Laibinis L, Byholm B, Pereverzeva I, Troubitsyna E, Tan KE, Porres I
Editors: Albert E, Sekerinski E
Publisher: Springer
Publication year: 2014
Publisher: Springer
Book title: Integrated Formal Methods, 11th International Conference, IFM 2014, Bertinoro, Italy, September 9-11, 2014, Proceedings
Title of series: Lecture Notes in Computer Science
Volume number: 8739
Start page: 103
End page: 119
ISBN: 978-3-319-10180-4
eISBN: 978-3-319-10181-1
ISSN: 0302-9743


Ensuring resilience of large data stores in the cloud is a challenging engineering issue. It requires the development techniques that allow the designers to predict the main resilience characteristics — fault tolerance and performance — at the early design stages. In this paper, we experiment with integrating Event-B modelling with discrete-event simulation. Event-B allows us to reason about correctness and data integrity properties of data stores, while discrete-event simulation in SimPy enables quantitative assessment of performance and reliability. Since testing in a real cloud environment is expensive and time-consuming, the proposed approach offers several benefits in industrial settings.


discrete-event simulation, Event-B, formal modelling

Last updated on 2020-05-06 at 05:30