Formal Analysis of Consensus Protocols

Organisation:	Technical University of Eindhoven (THE NETHERLANDS)
Method:	mCRL2
Tools used:	CADP (Construction and Analysis of Distributed Processes) mCRL2 toolset
Domain:	Distributed Algorithms.
Period:	2009
Size:	1,507,990 states and 45,329 states
Description:	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.
Conclusions:	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.
Publications:	[Atif-09] Muhammad Atif. "Formal Analysis of Consensus Protocols in Asynchronous Distributed Systems." 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 the CADP Web site in PDF or PostScript
Contact:	Muhammad Atif Department of Mathematics and Computer Science Eindhoven University of Technology P.O. Box 513 5600MB Eindhoven The Netherlands Phone: +31 402 474 425 Email: m.atif@tue.nl
Further remarks:	This case study, amongst others, is described on the CADP Web site: http://cadp.inria.fr/case-studies

Back to the CADP case studies page