On a Verification Framework for Certifying Distributed Algorithms: Distributed Checking and Consistency - Formal Techniques for Distributed Objects, Components, and Systems (FORTE 2018) Access content directly
Conference Papers Year : 2018

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

Kim Völlinger
  • Function : Author
  • PersonId : 1033826

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.
Fichier principal
Vignette du fichier
469043_1_En_9_Chapter.pdf (437.8 Ko) Télécharger le fichier
Origin : Files produced by the author(s)
Loading...

Dates and versions

hal-01824815 , version 1 (27-06-2018)

Licence

Attribution

Identifiers

Cite

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⟩
283 View
50 Download

Altmetric

Share

Gmail Facebook X LinkedIn More