Abstract

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.

Attachments:

ConsensusTLASpec.pdf

[ ]

583 Kb