Skip to Main content Skip to Navigation
Conference papers

On a Verification Framework for Certifying Distributed Algorithms: Distributed Checking and Consistency

Abstract : A major problem in software engineering is assuring the correctness of a distributed system. A certifying distributed algorithm (CDA) computes for its input-output pair (i, o) an additional witness w – a formal argument for the correctness of (i, o). Each CDA features a witness predicate such that if the witness predicate holds for a triple (i, o, w), the input-output pair (i, o) is correct. An accompanying checker algorithm decides the witness predicate. Consequently, a user of a CDA does not have to trust the CDA but its checker algorithm. Usually, a checker is simpler and its verification is feasible. To sum up, the idea of a CDA is to adapt the underlying algorithm of a program at design-time such that it verifies its own output at runtime. While certifying sequential algorithms are well-established, there are open questions on how to apply certification to distributed algorithms. In this paper, we discuss distributed checking of a distributed witness; one challenge is that all parts of a distributed witness have to be consistent with each other. Furthermore, we present a method for formal instance verification (i.e. obtaining a machine-checked proof that a particular input-output pair is correct), and implement the method in a framework for the theorem prover Coq.
Complete list of metadata

Cited literature [31 references]  Display  Hide  Download

https://hal.inria.fr/hal-01824815
Contributor : Hal Ifip <>
Submitted on : Wednesday, June 27, 2018 - 3:55:26 PM
Last modification on : Thursday, July 26, 2018 - 2:58:07 PM
Long-term archiving on: : Thursday, September 27, 2018 - 3:57:24 AM

File

469043_1_En_9_Chapter.pdf
Files produced by the author(s)

Licence


Distributed under a Creative Commons Attribution 4.0 International License

Identifiers

Citation

Kim Völlinger, Samira Akili. On a Verification Framework for Certifying Distributed Algorithms: Distributed Checking and Consistency. 38th International Conference on Formal Techniques for Distributed Objects, Components, and Systems (FORTE), Jun 2018, Madrid, Spain. pp.161-180, ⟨10.1007/978-3-319-92612-4_9⟩. ⟨hal-01824815⟩

Share

Metrics

Record views

754

Files downloads

3