@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}
}
Deductive Verification of a Byzantine Agreement Protocol
| Author(s): | Roman Krenický and Mattias Ulbrich |
|---|---|
| Institution: | Karlsruhe Institute of Technology, Department of Informatics |
| Number: | 2010-7 |
| Year: | 2010 |
| URL: | http://digbib.ubka.uni-karlsruhe.de/volltexte/1000017275 |
| Keywords: | Event-B Byzantine Agreement |
| Links: | Event-B sources |
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.