文章基本信息

标题：Proving Distributed Algorithms by Combining Reﬁnement and Local Computations
本地全文：下载
作者：Mohamed Tounsi ; Mohamed Mosbah ; Dominique Méry 等
期刊名称：Electronic Communications of the EASST
电子版ISSN：1863-2122
出版年度：2011
卷号：35
语种：English
出版社：European Association of Software Science and Technology (EASST)
摘要：Distributed algorithms are considered to be very complex to design and to prove; our paper contributes to the design of correct-by-construction distributed algorithms. The main idea relies upon the development of distributed algorithms following a top/down approach, which is clearly well known in earlier works of Dijkstra, and to use refinement for proving the correctness of the resulting algorithms. However, the link between the problem and the first model remains to be expressed and the refinement is a real help to justify in a very progressive way the choices of design. We propose in this work a framework combining local computations models and refinement to prove the correctness of a large class of distributed algorithms. Local computations models define abstract computing processes for solving problems by distributed algorithms and can be integrated into a the Event-B modelling language to define proof-based patterns for the design of distributed algorithms. We illustrate our approach by examples like the leader election protocol or the distributed coloring algorithm. Our proposal is integrated into an environment called ViSiDiA.