ISBN 978-3-8439-3325-4

978-3-8439-3325-4, Reihe Informationstechnik

Philipp Luithardt
Formale Validierung eines Verfahrens zur konsistenten Master/Shadow-Festlegung in einem verteilten, nicht uhrensynchronen Avioniksystem

285 Seiten, Dissertation Universität Stuttgart (2017), Softcover, B5

Zusammenfassung / Abstract

Digitale Avioniksysteme für sicherheitskritische Anwendungen sind charakterisiert durch hoch redundante Systemstrukturen in Verbindung mit komplexen Systemverwaltungsfunktionen, um so den fehlertoleranten Systembetrieb sicherzustellen. Die Entwicklung solcher Avioniksysteme ist in der Regel entsprechend herausfordernd. Vor diesem Hintergrund erarbeitet das Institut für Luftfahrtsysteme die so genannte Flexible Plattform, ein umfassender Ansatz zur plattformbasierten Entwicklung fehlertoleranter Rechnernetzwerke (sog. Plattforminstanzen), die als Basis für digitale Avioniksysteme dienen. Die Flexible Plattform umfasst neben anderem einen Baukasten generischer Verwaltungssoftware-Bausteine, durch deren anwendungsspezifische Instanziierung sich die oben genannten komplexen Systemverwaltungsfunktionen komfortabel generieren lassen.

Die vorliegende Arbeit befasst sich mit einem Teilaspekt dieser Verwaltungssoftware-Bausteine: einem verteilt ausgeführten Verfahren, welches in der charakteristischen Ablaufumgebung eines mittels der Flexiblen Plattform erstellten Avioniksystems die Steuerautorität zwischen zwei replizierten Berechnungseinheiten koordiniert und umsetzt. Diese Master/Shadow-Festlegung muss im Avioniksystem selbst unter Anwesenheit von Fehlern stets konsistent erfolgen. Ist dies nicht sichergestellt, birgt ein derartiger Mechanismus das Versagen des Avioniksystems in sich.

Im Rahmen dieser Arbeit wird der formale Nachweis erbracht, dass das in der Flexiblen Plattform vorgesehene Verfahren zur Master/Shadow-Festlegung in einer charakteristischen Plattforminstanz unter allen zu betrachtenden Fehlerfällen in hinreichend endlicher Zeit immer zu einer konsistenten Master/Shadow-Festlegung führt.