A Formally Verified Algorithm for Interactive Consistency Under a Hybrid Fault Model

Patrick Lincoln and John Rushby

Proceedings of the Fault-Tolerant Computing Symposium, FTCS 23, Toulouse, France, June 1993, pp. 402-411; also appears in FTCS: Highlights from 25 Years, 1995, pp. 438-447


Thambidurai and Park have proposed an algorithm for Interactive Consistency that retains resilience to the arbitrary (or Byzantine) fault mode, while tolerating more faults of simpler kinds than standard Byzantine-resilent algorithms. Unfortunately, and despite a published proof of correctness, their algorithm is flawed. We detected this while undertaking a formal verification of the algorithm.

We present a corrected algorithm that has been subjected to mechanically-checked formal verification. Because informal proofs seem unreliable in this domain, and the consequences of failure could be catastrophic, we believe formal verification should become standard for algorithms intended for safety-critical applications.




BibTeX Entry

@string{ftcs = {Fault Tolerant Computing Symposium }}
@string{ieeecs = {IEEE Computer Society}}

	AUTHOR = {Patrick Lincoln and John Rushby},
	TITLE = {A Formally Verified Algorithm for Interactive Consistency
		under a Hybrid Fault Model},
	PAGES = {402--411},
	NOTE = {Reprinted in~\cite[pp.\ 438--447]{FTCS-highlights}}

	KEY = {FTCS-23},
	BOOKTITLE = ftcs # 23,
	TITLE = ftcs # 23,
	MONTH = jun,
	YEAR = 1993,
	ADDRESS = {Toulouse, France},

	KEY = {FTCS-Highlights},
	TITLE = ftcs # 25 # {: Highlights from 25 Years},
	BOOKTITLE = ftcs # 25 # {: Highlights from 25 Years},
	YEAR = 1995,
	PUBLISHER = ieeecs,
	ADDRESS = {Pasadena, CA},
	MONTH = jun

Having trouble reading our papers?
Return to John Rushby's bibliography page
Return to the Formal Methods Program home page
Return to the Computer Science Laboratory home page