Certification formelle de la correction d'algorithmes distribués avec erreurs de transmission

Abstract : Computer systems fail. Whatever the reason of these failures, it has been a widespread approach to try and increase the faults-tolerance of a computer system through its replication. The resulting system is said to be a distributed one, in which replicas have to be kept consistent with each others. Hence, reaching agreement, and Consensus in particular, becomes the problem to solve - indeed, the paradigm. Solving Consensus (under various assumptions) is a hard task : algorithms designed on this purpose are subtle and proving their being correct is error-prone - whenever they are, which occasionally appears not to be the case. For more that thirty years, researchers interested in what is called Formal Methods have been working on mechanizing the verification process, in order to increase confidence in the correctness of (distributed) algorithms. The work we present here is at the intersection of distributed algorithms and formal methods. We use the Isabelle/HOL software to certify the correctness proof of various Consensus algorithms expressed in a uniform framework based on the Heard-Of Model, introduced by Charron-Bost and Schiper in 2009. Expressed in a common model, these algorithms, which, depending on the case, share some common mecanisms (number of steps, intermediate votes, ...), some elements of syntax, or types of assumptions (partial synchronism...), can be proved using some common arguments. As a consequence, the certification effort can be reduced by copying some intermediate lemmas from one proof to another and let the computer automatically parse them until some manual adaptation is required. This lead to the idea of certifying the correctness of multiple algorithms all together, instead of proving them one after the other, as one would do on paper in a traditional way. The effort of translation in the formal language of the proof assistant is then possibly reduced. Of course, each proof will also contain specific arguments, which will have to be isolated and translated into the software. Here, we illustrate this proposition through the presentation of formal certificates of correctness for six Consensus algorithms. As a consequence, on should not expect to find here a comprehensive linear presentation of each proof : we first show the arguments shared by multiple proofs, followed by those which are specific to each o them
Document type :
Theses
File URL :
http://docnum.univ-lorraine.fr/prive/DDOC_T_2013_0268_DEBRAT.pdf
Complete list of metadatas

https://hal.univ-lorraine.fr/tel-01750614
Contributor : Thèses Ul <>
Submitted on : Thursday, March 29, 2018 - 12:50:31 PM
Last modification on : Tuesday, April 24, 2018 - 1:30:19 PM

Identifiers

  • HAL Id : tel-01750614, version 1

Collections

Citation

Henri Debrat. Certification formelle de la correction d'algorithmes distribués avec erreurs de transmission. Autre [cs.OH]. Université de Lorraine, 2013. Français. ⟨NNT : 2013LORR0268⟩. ⟨tel-01750614⟩

Share

Metrics

Record views

19