Analysis of Self-* and P2P Systems using Refinement (Full Report)

Manamiary Bruno Andriamiarina 1, 2 Dominique Méry 1, 2 Neeraj Kumar Singh 3
1 MOSEL - Proof-oriented development of computer-based systems
LORIA - FM - Department of Formal Methods
2 VERIDIS - Modeling and Verification of Distributed Algorithms and Systems
MPII - Max-Planck-Institut für Informatik, Inria Nancy - Grand Est, LORIA - FM - Department of Formal Methods
Abstract : Distributed systems and applications require efficient and effective techniques (e.g. self (re)configuration, self-healing, etc.) for ensuring safety, security and more generally dependability properties, as well as convergence. The complexity of these systems is increased by features like dynamic (changing) topology, interconnection of heterogeneous components or failures detection. This paper presents a methodology for verifying protocols and satisfying safety and convergence requirements of the distributed self- systems. The self- systems are based on the idea of managing complex infrastructures, software, and distributed systems, with or without minimal user interactions. Correct-by-construction and service-as-event paradigms are used for formalizing the system requirements, where the formalization process is based on incremental refinement in EVENT B. Moreover, this paper describes a fully mechanized proof of correctness of the self-* systems along with an interesting case study related to the P2P-based self healing protocol.
Document type :
Reports
Liste complète des métadonnées

Cited literature [24 references]  Display  Hide  Download

https://hal.inria.fr/hal-01018162
Contributor : Manamiary Bruno Andriamiarina <>
Submitted on : Thursday, July 3, 2014 - 5:05:33 PM
Last modification on : Tuesday, February 19, 2019 - 3:40:03 PM
Document(s) archivé(s) le : Friday, October 3, 2014 - 11:56:02 AM

File

paperv1.pdf
Files produced by the author(s)

Identifiers

  • HAL Id : hal-01018162, version 1

Collections

Citation

Manamiary Bruno Andriamiarina, Dominique Méry, Neeraj Kumar Singh. Analysis of Self-* and P2P Systems using Refinement (Full Report). [Research Report] 2014. ⟨hal-01018162⟩

Share

Metrics

Record views

382

Files downloads

181