Ensuring resilience of large data stores in 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. Furthermore, Event-B modelling facilitates verification of the simulation model and increases the developer’s confidence in the design. Since testing a in a real cloud environment is expensive and time-consuming, the proposed approach offers several benefits in industrial settings.
Linas Laibinis , Benjamin Byholm (Abo Akademi University), Inna Pereverzeva (Åbo Akademi University, Turku Centre for Computer Science), Kuan Eeik Tan (F-Secure) , and Ivan Porres (Åbo Akademi University): Integrating Event-B Modelling and Discrete-Event Simulation to Analyse Resilience of Data Stores in the Cloud