Technical University of Eindhoven (THE NETHERLANDS)
CADP (Construction and Analysis of Distributed Processes)
1,507,990 states and 45,329 states
In a consensus protocol, each participating process proposes a value
and eventually all (non-crashed) processes should reach a state in
which they decide upon the same value, which has to be chosen from the
set of proposed values by the participating processes. In an
asynchronous environment, there is no upper bound on the delay of
(reliable) communication channels; hence, a process cannot distinguish
between a process who has crashed and a process connected to a very
slow communication channel. To circumvent this problem, the consensus
protocols are built upon failure detectors, which by a synchronization
mechanism can provide information about crashed (i.e., permanently
halted) and correct processes.
This work deals with the specification and verification of two consensus protocols. The first one uses strong completeness with weak accuracy and the other uses strong completeness with eventual weak accuracy. Strong completeness refers to suspecting all crashed processes, i.e., after a certain amount of time every correct process permanently suspects each crashed process. Weak accuracy means that some correct process is never suspected. Eventual weak accuracy means that after a certain amount of time, some correct process is never suspected.
The two consensus protocols were specified formally in mCRL2 and four correctness requirements were expressed in modal mu-calculus. The underlying state spaces were generated explicitly as BCG files and the four requirements were successfully verified on these state spaces using the EVALUATOR model checker of CADP. The requirements on the second protocol (which has a smaller number of transitions) could also be checked using a model checker of the mCRL2 toolset.
Two distributed algorithms for the consensus problem were formally
specified, together with their correctness requirements. A common
failure detector was devised, which satisfies weak accuracy and strong
completeness (or eventual strong completeness). The verification shown
that the two protocols satisfy the requirements.
"Formal Analysis of Consensus Protocols in Asynchronous Distributed
CS-Report 09-16, Technical University of Eindhoven,
34 pages, October 2009.
Available on-line at: http://www.win.tue.nl/~atif/reports/report0916.pdf
or from our FTP site in PDF or PostScript
Department of Mathematics and Computer Science
Eindhoven University of Technology
P.O. Box 513
Phone: +31 402 474 425
|Further remarks:||This case study, amongst others, is described on the CADP Web site: http://cadp.inria.fr/case-studies|