Formal Proofs of Termination Detection for Local Computations by Refinement-Based Compositions

Maha Boussabbeh, Mohamed Tounsi 0001, Mohamed Mosbah 0001, Ahmed Hadj Kacem
Digital Printed Abstract View Cite
Type
Conference paper
Publication
5th International Conference on ASM, Alloy, B, TLA, VDM, and Z (ABZ'16)

Abstract

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.

Document

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.

Reference

% BibTex
@inproceedings{BoussabbehTMK16,
  author       = {Maha Boussabbeh and
                  Mohamed Tounsi and
                  Mohamed Mosbah and
                  Ahmed Hadj Kacem},
  editor       = {Michael J. Butler and
                  Klaus{-}Dieter Schewe and
                  Atif Mashkoor and
                  Mikl{\'{o}}s Bir{\'{o}}},
  title        = {Formal Proofs of Termination Detection for Local Computations by Refinement-Based
                  Compositions},
  booktitle    = {Abstract State Machines, Alloy, B, TLA, VDM, and {Z} - 5th International
                  Conference, {ABZ} 2016, Linz, Austria, May 23-27, 2016, Proceedings},
  series       = {Lecture Notes in Computer Science},
  volume       = {9675},
  pages        = {198--212},
  publisher    = {Springer},
  year         = {2016},
  url          = {https://doi.org/10.1007/978-3-319-33600-8\_12},
  doi          = {10.1007/978-3-319-33600-8\_12},
  timestamp    = {Tue, 11 Oct 2022 14:59:07 +0200},
  biburl       = {https://dblp.org/rec/conf/asm/BoussabbehTMK16.bib},
  bibsource    = {dblp computer science bibliography, https://dblp.org}
}
ABZ'16

Related