Analysis of Self-* and P2P Systems using Refinement

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 : Abstract. Distributed systems and applications are becoming increasingly complex, due to factors such as dynamic topology, heterogeneity of components, failure detection. Therefore, they require effective techniques for guaranteeing safety, security and convergence. The self- systems are based on the idea of managing efficiently complex systems and architectures without user interaction. This paper presents a methodology for verifying distributed systems and ensuring safety and convergence requirements: Correct-by-construction and service-as-event paradigms are used for formalizing the system requirements using incremental refinement in E VENT B. Moreover, this paper describes a mechanized proof of correctness of the self- systems along with a case study related to the P2P-based self-healing protocol.
Document type :
Conference papers
Complete list of metadatas

https://hal.inria.fr/hal-01018125
Contributor : Manamiary Bruno Andriamiarina <>
Submitted on : Thursday, July 3, 2014 - 4:22:39 PM
Last modification on : Thursday, September 19, 2019 - 5:00:11 PM

Identifiers

Collections

Citation

Manamiary Bruno Andriamiarina, Dominique Méry, Neeraj Kumar Singh. Analysis of Self-* and P2P Systems using Refinement. ABZ 2014 - 4th International ABZ 2014 Conference ASM, Alloy, B, TLA, VDM, Z, Yamine AIT AMEUR and Klaus-Dieter SCHEWE, Jun 2014, Toulouse, France. pp.117-123, ⟨10.1007/978-3-662-43652-3_9⟩. ⟨hal-01018125⟩

Share

Metrics

Record views

320