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 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.
Access provided by Autonomous University of Puebla. Download to read the full chapter text
Chapter PDF
Similar content being viewed by others
Keywords
References
Abrial, J.-R.: Modeling in Event-B: System and Software Engineering. Cambridge University Press (2010)
Andriamiarina, M.B., Méry, D., Singh, N.K.: Integrating Proved State-Based Models for Constructing Correct Distributed Algorithms. In: Johnsen, E.B., Petre, L. (eds.) IFM 2013. LNCS, vol. 7940, pp. 268–284. Springer, Heidelberg (2013)
Andriamiarina, M.B., Méry, D., Singh, N.K.: Analysis of Self-⋆ and P2P Systems using Refinement (Full Report). Technical Report, LORIA, Nancy, France (2014)
Berns, A., Ghosh, S.: Dissecting self-* properties. In: Proceedings of the 2009 Third IEEE International Conference on Self-Adaptive and Self-Organizing Systems, SASO 2009, pp. 10–19. EEE Computer Society, Washington, DC (2009)
Dolev, S.: Self-Stabilization. MIT Press (2000)
Lamport, L.: A temporal logic of actions. ACM Trans. Prog. Lang. Syst. 16(3), 872–923 (1994)
Leavens, G.T., Abrial, J.-R., Batory, D.S., Butler, M.J., Coglio, A., Fisler, K., Hehner, E.C.R., Jones, C.B., Miller, D., Jones, S.L.P., Sitaraman, M., Smith, D.R., Stump, A.: Roadmap for enhanced languages and methods to aid verification. In: Jarzabek, S., Schmidt, D.C., Veldhuizen, T.L. (eds.) GPCE, pp. 221–236. ACM (2006)
Marquezan, C.C., Granville, L.Z.: Self-* and P2P for Network Management - Design Principles and Case Studies. Springer Briefs in Computer Science. Springer (2012)
Méry, D.: Refinement-based guidelines for algorithmic systems. International Journal of Software and Informatics 3(2-3), 197–239 (2009)
Méry, D., Singh, N.K.: Automatic code generation from event-b models. In: Proceedings of the Second Symposium on Information and Communication Technology, SoICT 2011, pp. 179–188. ACM, New York (2011)
Smith, G., Sanders, J.W.: Formal development of self-organising systems. In: González Nieto, J., Reif, W., Wang, G., Indulska, J. (eds.) ATC 2009. LNCS, vol. 5586, pp. 90–104. Springer, Heidelberg (2009)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2014 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Andriamiarina, M.B., Méry, D., Singh, N.K. (2014). Analysis of Self-⋆ and P2P Systems Using Refinement. In: Ait Ameur, Y., Schewe, KD. (eds) Abstract State Machines, Alloy, B, TLA, VDM, and Z. ABZ 2014. Lecture Notes in Computer Science, vol 8477. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-662-43652-3_9
Download citation
DOI: https://doi.org/10.1007/978-3-662-43652-3_9
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-662-43651-6
Online ISBN: 978-3-662-43652-3
eBook Packages: Computer ScienceComputer Science (R0)