Publikation
Zertifizierung einer Sicherungskomponente mittels durchgängig formaler Modellierung
Udo Frese; Daniel Hausmann; Christoph Lüth; Holger Täubig; Dennis Walter
In: Walid Maalej; Bernd Brügge (Hrsg.). Software Engineering 2008 - Workshopband: Fachtagung des GI-Fachbereichs Softwaretechnik. GI-Fachtagungen, February 18-22, München, Germany, Pages 335-338, Lecture Notes in Informatics (LNI), Vol. P-122, ISBN 978-3-88579-216-1, Gesellschaft für Informatik, 2008.
Zusammenfassung
Dieses Papier berichtet über Arbeiten im Rahmen des Projektes SAMS, in welchem eine
Fahrwegsicherungskomponente für Serviceroboter und fahrerlose Transportsysteme entwickelt
und ihre Software nach IEC 61508 zertifiziert wird. Neu ist hierbei der durchgehende
Einsatz formaler Modellierung und Beweis als Mittel zur Zertifizierung, das es uns
erlaubt, die erforderlichen Sicherheitsbedingungen sehr abstrakt mathematisch zu formulieren,
und gleichzeitig den Bezug zur Implementierung bewiesen korrekt herzustellen.
Indem wir die Grundlagen der Anwendungsdomäne (Geometrie und die Mechanik bewegter
Objekte) in einem Theorembeweiser formalisieren, können wir die Sicherheitsanforderungen
auf einer abstrakten, mathematischen Ebene formulieren. Diese sind dann wesentlich
leichter zu validieren als implementationsnah formulierte Programmeigenschaften.
Darüber hinaus modellieren wir die Implementierung innerhalb desselben formalen Rahmens.
Dadurch erhalten wir einen nahtlosen Entwicklungsprozess mit einem klaren und
beweisbar korrekten Übergang von den Sicherheitseigenschaften zu der Implementation.
Wir glauben, dass diese Vorgehensweise für alle Sicherheitszertifikationen nützlich sein
kann: die formale Modellierung erzwingt, dass alle Annahmen, die in den Sicherheitsanforderungen,
der Implementation oder den Beweisen implizit enthalten sind, explizit
gemacht werden, so dass sich der Zertifikationsprozess auf die Sicherheitsanforderungen
konzentrieren kann, da die Korrektheitsbeweise automatisch geprüft werden können.