FCPre: Extending the Arora-Kulkarni Method of Automatic Addition of Fault-Tolerance
| URN | urn:nbn:de:gbv:18-228-7-170 |
|---|---|
| URL | http://edoc.sub.uni-hamburg.de/informatik/volltexte/2009/17/ |
| Dokumentart: | Report (Bericht) |
| Schriftenreihe: | Berichte des Fachbereichs Informatik der Universität Hamburg |
| Bandnummer: | 275 |
| Sprache: | Englisch |
| Erstellungsjahr: | 2006 |
| Publikationsdatum: | 28.04.2009 |
| SWD-Schlagwörter: | Fehlertoleranz |
| DDC-Sachgruppe: | Informatik |
| BK - Klassifikation: | 54.32 |
Kurzfassung auf Englisch:
Synthesizing fault-tolerant systems from fault-intolerant systems simplifies design of fault-tolerance. Arora and Kulkarni developed a method and tool to synthesize fault-tolerance under the assumption that specifications are not history-dependent (fusion-closed). Later, Gaertner and Jhumka removed this assumption by presenting a modular extension of the Arora-Kulkarni method. This paper presents an implementation of the Gaertner-Jhumka method which is evaluated on several examples. As additional safety net, we added automatic verification of the results using the model checker Spin. In the context of this work, a fault in the Gaertner-Jhumka-method was found. Though this fault is rare and does not cause incorrect results, there might be no result.
Kurzfassung auf Deutsch:
Die Synthese fehlertoleranter Systeme aus fehlerintoleranten Systemen erleichtert die Generierung von Fehlertoleranz. Es existiert bereits ein Verfahren, um bestehende Programme nachträglich fehlertolerant zu machen, die Arora-Kulkarni-Methode. Dafür wird ein neues Programm generiert, dem ein Fehlertoleranz-Mechanismus hinzugefügt wurde. Dieses Verfahren ist allerdings sehr restriktiv hinsichtlich der möglichen Eingaben. So werden nur sogenannte fusion closed Spezifikationen akzeptiert. In dieser Arbeit wird die Implementation eines neuen Verfahrens präsentiert, das auch andere Spezifikationen akzeptiert, die Gärtner-Jhumka-Methode. Dieses Verfahren funktioniert als Vorverarbeitung und gibt ein Zwischenprogramm aus, das die restriktiven Anforderungen der Arora-Kulkarni-Methode erfüllt. Der Rest der Fehlertoleranz-Synthese kann schliesslich von dieser geleistet werden. Um das Vertrauen in die Ausgaben der Synthese zu erhöhen, werden sie jeweils durch den Model Checker Spin verifiziert. Im Rahmen dieser Arbeit wurde ein Fehler in der Gärtner-Jhumka-Methode festgestellt. Dieser Fehler tritt nur selten auf und führt nicht zu fehlerhaften Ergebnissen. Allerdings ist er in einigen Fällen dafür verantwortlich, dass gar kein Ergebnis berechnet werden kann.
Hinweis zum Urherberrecht
Für Dokumente, die in elektronischer Form über Datenenetze angeboten werden, gilt uneingeschränkt das Urheberrechtsgesetz (UrhG). Insbesondere gilt:
Einzelne Vervielfältigungen, z.B. Kopien und Ausdrucke, dürfen nur zum privaten und sonstigen eigenen Gebrauch angefertigt werden (Paragraph 53 Urheberrecht). Die Herstellung und Verbreitung von weiteren Reproduktionen ist nur mit ausdrücklicher Genehmigung des Urhebers gestattet.
Der Benutzer ist für die Einhaltung der Rechtsvorschriften selbst verantwortlich und kann bei Mißbrauch haftbar gemacht werden.