The task is to find a suitable model for verification purposes of distributed algorithms. As an example we verified the S algorithm of Chandra/Toug within the theorem proving environment Isabelle/HOL. We first designed a TLA+ model and adopted and extended this model to formally show the three consensus properties Validity, Agreement and Termination.

Download this file (ConsensusTLASpec.pdf)ConsensusTLASpec.pdf[ ]583 Kb