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 Event 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.
If you cannot see the document below, the PDF document is most likely not freely accessible. In this case, please try to access the document via this link.
% BibTex
@inproceedings{AndriamiarinaMS14,
author = {Manamiary Bruno Andriamiarina and
Dominique M{\'{e}}ry and
Neeraj Kumar Singh},
editor = {Yamine A{\"{\i}}t Ameur and
Klaus{-}Dieter Schewe},
title = {Analysis of Self-{\(\star\)} and {P2P} Systems Using Refinement},
booktitle = {Abstract State Machines, Alloy, B, TLA, VDM, and {Z} - 4th International
Conference, {ABZ} 2014, Toulouse, France, June 2-6, 2014. Proceedings},
series = {Lecture Notes in Computer Science},
volume = {8477},
pages = {117--123},
publisher = {Springer},
year = {2014},
url = {https://doi.org/10.1007/978-3-662-43652-3\_9},
doi = {10.1007/978-3-662-43652-3\_9},
timestamp = {Thu, 10 Nov 2022 08:51:52 +0100},
biburl = {https://dblp.org/rec/conf/asm/AndriamiarinaMS14.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}