Formal Proofs for Broadcast Algorithms

Authors: Mandy Zammit, Adrian Francalanza

Corresponding: Mandy Zammit (mandy.zammit.08@um.edu.mt)

Keywords: Distributed Algorithms, Broadcast Algorithms, Correctness

Doi: http://dx.medra.org/10.7423/XJENZA.2014.2.04

Issue: Xjenza Online Vol. 2 Iss. 2 - October 2014

Abstract:
Standard distributed algorithmic solutions to recurring distributed problems are commonly specied and described informally. A proper understanding of these distributed algorithms that claries ambiguities requires formal descriptions. However, formalisation tends to yield complex descriptions. We formally study two broadcast algorithms and present an encoding framework using a process descriptive language and formalise these algorithms and their specications using this framework. Following these new formal encodings we discuss correctness proofs for the same algorithms.

Download Article: