Where academic tradition
meets the exciting future

You are here: TUCS > PUBLICATIONS > Publication Search > Formal Modelling of Resilient ...

Formal Modelling of Resilient Data Storage in Cloud

Inna Pereverzeva, Linas Laibinis, Elena Troubitsyna, Markus Holmberg, Mikko Pöri, Formal Modelling of Resilient Data Storage in Cloud. In: Lindsay Groves, Jing Sun (Eds.), Proceedings of 15th 1. 15th International Conference on Formal Engineering Methods, Lecture Notes in Computer Science, 364–380, Springer-Verlag Berlin Heidelberg, 2013.

Abstract:

Reliable and highly performant handling of large data stores constitutes one of the major challenges of cloud computing. In this paper, we propose a formalisation of a cloud solution implemented by F-Secure – a provider of secure data storage services. The solution is based on massive replication and the write-ahead logging mechanism. To achieve high performance, the company has abandoned a transactional model. We formally derive a model of the proposed architectural solution and verify data integrity and consistency properties under possible failure scenarios. The proposed approach allows the designers to formally define and verify essential characteristics of architectures for handling large data stores.

BibTeX entry:

@INPROCEEDINGS{inpPeLaTrHoPx13a,
  title = {Formal Modelling of Resilient Data Storage in Cloud},
  booktitle = {Proceedings of 15th 1. 15th International Conference on Formal Engineering Methods},
  author = {Pereverzeva, Inna and Laibinis, Linas and Troubitsyna, Elena and Holmberg, Markus and Pöri, Mikko},
  series = {Lecture Notes in Computer Science},
  editor = {Groves, Lindsay and Sun, Jing},
  publisher = {Springer-Verlag Berlin Heidelberg},
  pages = {364–380},
  year = {2013},
  keywords = {Formal modelling, Event-B, refinement, replication, data integrity, large data stores.},
}

Belongs to TUCS Research Unit(s): Distributed Systems Laboratory (DS Lab)

Publication Forum rating of this publication: level 1

Edit publication