In der vorliegenden Arbeit wird ein Algorithmus für verteilte Einigung (“PerfectFDAgreement”) in Java implementiert. Bei PerfetFDAgreement handelt es sichh um einen Algorithmus der zwischhen mehreren Prozessen Konsens ermöglicht, auchh wenn einige der teilnehmenden Prozesse stoppen. Deswegen ist ein Failure Detector Teil des Algorithmus, welchher die Prozesse über gestoppte Prozesse informiert, so daß diese die gestoppten Prozesse in ihrer Entschheidungsfindung nicht mehr beachten.
Der Algorithmus wird zunächst formal als Automat beschhrieben. Die Transitionen dieses Automaten stellen die Methoden der entsprechenden Java-Klasse dar. Die Implementierung umfasst die Prozesse, den Failure Detector und den Broadcast Channel über den die Kommunikation der Prozesse läuft. Die Kommunikation zwischen den Prozessen wird dabei als zuverlässig angenommen.
Die Implementierung wurde anschliessend mit Zusicherungen annotiert um die Korrektheit des Algorithmus zu garantieren. Der Korrektheitsbeweis wurde stellenweise ausgeführt. Im Schluss wird ein Ausblick auf die Möglichkeit der maschinellen Durchführung des Beweises gegeben.
| supervisors | Martin Steffen |