Home | deutsch  | Legals | Sitemap | KIT

Deductive Verification of a Byzantine Agreement Protocol

Deductive Verification of a Byzantine Agreement Protocol
Author(s):

Roman Krenický
Mattias Ulbrich

Links:
Source:

digital library of the KIT

Date: April 2010

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.

Download the sources for the Rodin tool.

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 Computer Science},
year = {2010},
number = {2010-7},
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},
}