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 条
  • [11] DISTRIBUTED DEADLOCK DETECTION
    CHANDY, KM
    MISRA, J
    HAAS, LM
    [J]. ACM TRANSACTIONS ON COMPUTER SYSTEMS, 1983, 1 (02): : 144 - 156
  • [12] DISTRIBUTED SNAPSHOTS - DETERMINING GLOBAL STATES OF DISTRIBUTED SYSTEMS
    CHANDY, KM
    LAMPORT, L
    [J]. ACM TRANSACTIONS ON COMPUTER SYSTEMS, 1985, 3 (01): : 63 - 75
  • [13] Courtieu P., 2015, ABS150601603 CORR
  • [14] TERMINATION DETECTION FOR DIFFUSING COMPUTATIONS
    DIJKSTRA, EW
    SCHOLTEN, CS
    [J]. INFORMATION PROCESSING LETTERS, 1980, 11 (01) : 1 - 4
  • [15] Towards Proved Distributed Algorithms Through Refinement, Composition and Local Computations
    Filou, Vinvent
    Mosbah, Mohamed
    Tounsi, Mohamed
    [J]. 2013 IEEE 22ND INTERNATIONAL WORKSHOP ON ENABLING TECHNOLOGIES: INFRASTRUCTURE FOR COLLABORATIVE ENTERPRISES (WETICE), 2013, : 353 - 358
  • [16] Godard E, 2002, LECT NOTES COMPUT SC, V2505, P106
  • [17] Iliasov A, 2010, LECT NOTES COMPUT SC, V5977, P174, DOI 10.1007/978-3-642-11811-1_14
  • [18] LEAVENS GT, 2006, P 5 INT C GEN PROGR, P221
  • [19] Litovsky I., 1999, HDB GRAPH GRAMMARS C, V3, P1
  • [20] Distributed enumeration
    Mazurkiewicz, A
    [J]. INFORMATION PROCESSING LETTERS, 1997, 61 (05) : 233 - 239
123