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

被引：1
作者：
Boussabbeh, Maha [1 ,2 ]
Tounsi, Mohamed [2 ]
Mosbah, Mohamed [1 ]
Kacem, Ahmed Hadj [2 ]
机构：
[1] Univ Bordeaux, LaBRI Lab, Talence, France
[2] Univ Sfax, ReDCAD Lab, Sfax, Tunisia
来源：
ABSTRACT STATE MACHINES, ALLOY, B, TLA, VDM, AND Z (ABZ 2016) | 2016年 / 9675卷
关键词：
Distributed algorithms; Local computations; Termination detection; SSP algorithm; Composition; Event-B method; EVENT-B; ALGORITHMS; SYSTEMS;
D O I：
10.1007/978-3-319-33600-8_12
中图分类号：
TP31 [计算机软件];
学科分类号：
081202 ; 0835 ;
摘要：
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.
引用
收藏
页码：198 / 212
页数：15
相关论文
共 24 条
  • [1] Rodin: An open toolset for modelling and reasoning in Event-B
    Abrial J.-R.
    Butler M.
    Hallerstede S.
    Hoang T.S.
    Mehta F.
    Voisin L.
    [J]. International Journal on Software Tools for Technology Transfer, 2010, 12 (06) : 447 - 466
  • [2] Revisiting Snapshot Algorithms by Refinement-based Techniques
    Andriamiarina, Manamiary Bruno
    Mery, Dominique
    Singh, Neeraj Kumar
    [J]. COMPUTER SCIENCE AND INFORMATION SYSTEMS, 2014, 11 (01) : 251 - 270
  • [3] [Anonymous], 2010, Modeling in Event-B: system and software engineering
  • [4] Bauderon M., 2003, ELECT NOTES THEOR CO, V72, P13
  • [5] Boussabbeh M., 2016, 24 EUR INT C PAR DIS
  • [6] Cansell D, 2008, MONOGR THEOR COMPUT, P47, DOI 10.1007/978-3-540-74107-7_3
  • [7] Casteran P., 2011, STUDIA INFORM UNIVER, V9, P39
  • [8] Chalopin J, 2008, LECT NOTES COMPUT SC, V5218, P47, DOI 10.1007/978-3-540-87779-0_4
  • [9] Election in partially anonymous networks with arbitrary knowledge in message passing systems
    Chalopin, Jeremie
    Godard, Emmanuel
    Metivier, Yves
    [J]. DISTRIBUTED COMPUTING, 2012, 25 (04) : 297 - 311
  • [10] Chandy K.M., 1989, Parallel program design
123