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 the Cloud

Inna Pereverzeva, Linas Laibnis, Elena Troubitsyna, Markus Holmberg, Mikko Pöri, Formal Modelling of Resilient Data Storage in the Cloud. TUCS Technical Reports 1076, 978-952-12-2887-2, 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 solution implemented by F-Secure - a provider of secure data storage services. The solution is based on massive replication and write-ahead logging mechanism. The company has abandoned transactional model to achieve high performance. We formally derive a model of the proposed architectural solution and verify data integrity properties under possible failure scenarios. The proposed approach allows the designers to formally define and verify the essential characteristics of architectures for handling large data stores.

Files:

Full publication in PDF-format

BibTeX entry:

@TECHREPORT{tPeLaTrHoPx13a,
  title = {Formal Modelling of Resilient Data Storage in the Cloud},
  author = {Pereverzeva, Inna and Laibnis, Linas and Troubitsyna, Elena and Holmberg, Markus and Pöri, Mikko},
  number = {1076},
  series = {TUCS Technical Reports},
  publisher = {978-952-12-2887-2},
  year = {2013},
  keywords = {Formal modelling, Event-B, refinement, replication, data integrity, large data stores},
  ISBN = {Turku Centre for Computer Scie},
}

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

Edit publication