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

Linas Laibinis, Benjamin Byholm, I Pereverzeva, Elena Troubitsyna, KE Tan, Ivan Porres Paltor

    Research output: Chapter in Book/Conference proceedingConference contributionScientificpeer-review

    4 Citations (Scopus)


    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.
    Original languageUndefined/Unknown
    Title of host publicationIntegrated Formal Methods, 11th International Conference, IFM 2014, Bertinoro, Italy, September 9-11, 2014, Proceedings
    EditorsE Albert, E Sekerinski
    ISBN (Electronic)978-3-319-10181-1
    ISBN (Print)978-3-319-10180-4
    Publication statusPublished - 2014
    MoE publication typeA4 Article in a conference publication
    Eventconference; 2014-09-09; 2014-09-11 - Bertinoro, Italy
    Duration: 9 Sept 201411 Sept 2014


    Conferenceconference; 2014-09-09; 2014-09-11


    • Event-B
    • discrete-event simulation
    • formal modelling

    Cite this