Software enthält Fehler. Fehler in technischen Systemen können fatale Folgen haben. Diese Auswirkungen reichen von wirtschaftlichen Nachteilen bedingt durch Rückrufaktionen bei Massenprodukten, wie z.B. bei Kraftfahrzeugen, bis zu Unfällen mit hohen Sach- und/oder Personenschäden [Lev95].

Die Entwicklung von Systemen mit Sicherheitsverantwortung wird von einer Sicherheitsanalyse bzw. einem Sicherheitsnachweis begleitet, die von einer Aufsichts- oder Zulassungsbehörde abgenommen werden muß. Sehr häufig werden für die Sicherheitsanalyse und die Entwicklung eines Systems zwei unabhängige Ansätze verfolgt.

So kann die Sicherheitsanalyse z.B. mit der Fehler-Möglichkeits- und Einfluß-Analyse (FMEA) unter Berücksichtigung der von [VDA96] empfohlenen Vorgehensweise erfolgen. Ziel ist die Steigerung der Funktionssicherheit und Zuverlässigkeit durch präventive Fehlervermeidung. Deshalb erfolgt hier die Identifizierung sicherheitskritischer Systemelemente inklusive möglicher Fehlerursachen und Auswirkungen. Während einer System-FMEA werden Funktionen und Fehlfunktionen im System ausschließlich umgangssprachlich beschrieben. Dies hat den Nachteil, daß die Bedeutung seitens des Lesers Interpretationsspielräume zuläßt und somit eine Quelle für Fehler sein kann. Vorteilhaft ist die für komplexe Systeme geeignete analytische und strukturierte Vorgehensweise bei der Sicherheitsanalyse.

Die Entwicklung von Systemen mit Sicherheitsverantwortung kann mit Hilfe formaler Methoden vorgenommen werden. Das zugehörige Softwaresystem kann ebenfalls formal entwickelt werden. Auf diese Weise können die Systeme zwar nicht fehlerfrei erstellt werden, das Vertrauen in die korrekte Funktion kann damit aber erheblich gesteigert werden. Bestandteil der formalen Entwicklung ist die formale Verifikation eines funktionalen Systemmodells gegenüber einem Sicherheitsmodell (einer Menge von Sicherheitseigenschaften). Das hierfür benötigte Sicherheitsmodell wird in den meisten Fällen aus dem Lasten- bzw. Pflichtenheft extrahiert oder sogar ad-hoc aufgestellt.

In dem Beitrag wird ein Lösungsweg vorgeschlagen, wie eine konventionelle System-FMEA um formale Anteile ergänzt werden kann, um dann daraus ein formales Sicherheitsmodell für die Verifikation von Sicherheitseigenschaften abzuleiten. Für die Beschreibung von Sicherheitseigenschaften kann Prädikaten- oder für reaktive Systeme Temporallogik verwendet werden. Diese Vorgehensweise ermöglicht die Definition der Sicherheitsbedingungen im Kontext des Systems, d.h. die für formale Spezifikation notwendigen Informationen werden zunächst auf allen Systemebenen zur Verfügung gestellt. Damit erfolgt die formale Spezifikation je nach Bedarf auf verschiedenen Abstraktionsstufen und immer sehr nahe an der tatsächlichen Systemfunktionalität. Außerdem erlaubt sie die Verfolgung der Sicherheitsanforderungen hinab bis zur Implementierung (Soft- und Hardware).