In this paper, we propose a formal framework enhancing the termination detection property of distributed algorithms and reusing their specifications as well as their proofs. By relying on refinement and composition, we show that an algorithm specified with local termination detection, can be reused in order to compute the same algorithm with global termination detection. The main idea relies upon the development of distributed algorithms following a top/down approach and the integration of additional computation steps developed in a pre-defined module. This module is specified in a generic and scalable way in order to be composed with particular developments. Once the composition link is proven, the global termination emerges automatically.
CITATION STYLE
Boussabbeh, M., Tounsi, M., Mosbah, M., & Kacem, A. H. (2016). Formal proofs of termination detection for local computations by refinement-based compositions. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 9675, pp. 198–212). Springer Verlag. https://doi.org/10.1007/978-3-319-33600-8_12
Mendeley helps you to discover research relevant for your work.