Deductive Verification of a Byzantine Agreement Protocol

Technical Report

Author(s):Roman Krenický and Mattias Ulbrich
Institution:Karlsruhe Institute of Technology, Department of Informatics
Year:2010
Number:2010-7
URL:http://digbib.ubka.uni-karlsruhe.de/volltexte/1000017275
Keywords: Event-B Byzantine Agreement
Links:

Abstract

This report describes a formalisation and deductive verification of a Byzantine Agreement Protocol. The model evolves over twelve steps of refinement each introducing a new aspect. The Event-B method is used to model the protocol, and the publicly available tool Rodin is used to deductively prove its correctness.

BibTeX

@TECHREPORT{KrenickyUlbrich2010,
  author = {Roman Krenick{\'y} and Mattias Ulbrich},
  title = {Deductive Verification of a Byzantine Agreement Protocol},
  institution = {Karlsruhe Institute of Technology, Department of Informatics},
  year = {2010},
  number = {2010-7},
  month = {April},
  abstract = {This report describes a formalisation and deductive verification of
	a Byzantine Agreement Protocol. The model evolves over twelve steps
	of refinement each introducing a new aspect. The Event-B method is
	used to model the protocol, and the publicly available tool Rodin
	is used to deductively prove its correctness.},
  keywords = {Event-B, Byzantine Agreement},
  links = {Event-B sources:http://lfm.iti.kit.edu/files/publications/ByzantineRodin.zip},
  url = {http://digbib.ubka.uni-karlsruhe.de/volltexte/1000017275}
}