Publication

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 (editor). 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) P-122 ISBN 978-3-88579-216-1 Gesellschaft für Informatik 2008.

Abstract

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.

Projekte

softzert08.pdf (pdf, 91 KB)

German Research Center for Artificial Intelligence
Deutsches Forschungszentrum für Künstliche Intelligenz