Open Access

Andreas Thums

• Diese Arbeit integriert die Sicherheitsanalysetechnik 'Fehlerbaumanalyse' (FTA) aus dem Bereich der Ingenieurwissenschaften in 'formale Methoden' aus dem Bereich der Softwaretechnik. Wir nennen diesen integrierten Ansatz 'formale FTA'. Die klassische FTA untersucht die Ausfallsicherheit von Systemen, während die formalen Methoden auf die funktionale Korrektheit fokussieren. Die formale FTA verknüpft die zwei, in ihrem jeweiligen Anwendungsgebiet bewährten, Techniken zu einer durchgängigen Analysemethode für Spezifikationen sicherheitskritischer Anwendungen. Das Anwendungsgebiet der formalen FTA sind softwarebasierte, eingebettete Systeme. Die Integration der FTA in formale Methoden besteht in der Definition einer formalen Semantik. Um die dynamischen Aspekte softwarebasierter eingebetteter Systeme abbilden zu können, wird die FTA-Semantik in Intervalltemporallogik (ITL) definiert. Aus der FTA-Semantik lassen sich Bedingungen ableiten, deren Nachweis garantiert, dass die FTA vollständigDiese Arbeit integriert die Sicherheitsanalysetechnik 'Fehlerbaumanalyse' (FTA) aus dem Bereich der Ingenieurwissenschaften in 'formale Methoden' aus dem Bereich der Softwaretechnik. Wir nennen diesen integrierten Ansatz 'formale FTA'. Die klassische FTA untersucht die Ausfallsicherheit von Systemen, während die formalen Methoden auf die funktionale Korrektheit fokussieren. Die formale FTA verknüpft die zwei, in ihrem jeweiligen Anwendungsgebiet bewährten, Techniken zu einer durchgängigen Analysemethode für Spezifikationen sicherheitskritischer Anwendungen. Das Anwendungsgebiet der formalen FTA sind softwarebasierte, eingebettete Systeme. Die Integration der FTA in formale Methoden besteht in der Definition einer formalen Semantik. Um die dynamischen Aspekte softwarebasierter eingebetteter Systeme abbilden zu können, wird die FTA-Semantik in Intervalltemporallogik (ITL) definiert. Aus der FTA-Semantik lassen sich Bedingungen ableiten, deren Nachweis garantiert, dass die FTA vollständig durchgeführt wurde, also keine Ausfallursachen bei der Analyse übersehen wurden. Um diese FTA-Bedingungen über einer Spezifikation softwarebasierter eingebetteter Systeme nachweisen zu können, wird eine Spezifikationssprache benötigt, die dynamische Aspekte dieser Systeme abbilden kann und ebenso den Nachweis der FTA-Bedingungen in ITL ermöglicht. Dazu werden Statecharts in ITL integriert, ein Beweiskalkül entwickelt und prototypisch implementiert. Das interaktive Verifikationswerkzeug KIV dient dabei als Entwicklungsplattform. Es können nun FTA-Bedingungen über Statechart-Spezifikationen nachgewiesen werden. Die Besonderheit des Statechart-Kalküls ist, dass er algebraisch spezifizierte Datentypen in Statechart-Spezifikationen erlaubt und damit sehr allgemeine und insbesondere nicht zustandsendliche Datentypen in Statecharts verwendet werden können. Die Arbeit wird durch eine Anwendungsmethodik für die formale FTA abgerundet, die durch ein Werkzeug unterstützt wird. Es wurde die Möglichkeit geschaffen, Fehlerbäume über Statechart-Spezifikationen in KIV zu erstellen und die Beweisbedingungen für die formale FTA zu erzeugen. Die Beweisbedingungen können dann mit dem entstandenen Statechart-Kalkül nachgewiesen werden. Damit ist eine vollständige methodische und werkzeugseitige Unterstützung für die formale FTA entstanden.…
• This work integrates the saftey analysis technique 'fault tree analysis' (FTA) from the engineering domain in 'formal methods' form software engineering. We call this integrated approach 'formal safety analysis'. While classical FTA focuses on failures, formal methods focus on functional correctness. Formal FTA combines these two approved methods to an integrated analysis method for specifying safety critical applications. The application domains of formal FTA are software based, embedded systems. The integration of FTA in formal methods consists of the definition of a formal semantics. To cope with the dynamic aspects of softwarebased embedded systems, the FTA semantics will be defined in interval temporal logic (ITL). The FTA semantics defines verification conditions. The proof of these verification conditions guarantees, that the application of FTA was complete, i.e. no failure condition was overlooked. To prove the FTA conditions over a specification for software based embeddedThis work integrates the saftey analysis technique 'fault tree analysis' (FTA) from the engineering domain in 'formal methods' form software engineering. We call this integrated approach 'formal safety analysis'. While classical FTA focuses on failures, formal methods focus on functional correctness. Formal FTA combines these two approved methods to an integrated analysis method for specifying safety critical applications. The application domains of formal FTA are software based, embedded systems. The integration of FTA in formal methods consists of the definition of a formal semantics. To cope with the dynamic aspects of softwarebased embedded systems, the FTA semantics will be defined in interval temporal logic (ITL). The FTA semantics defines verification conditions. The proof of these verification conditions guarantees, that the application of FTA was complete, i.e. no failure condition was overlooked. To prove the FTA conditions over a specification for software based embedded systems a specification language is necessary, which can cope with the dynamic aspects of these systems and additionally allows the verification of the FTA conditions in ITL. Therefore, statecharts are integrated in ITL and an corresponding proof calculus will be developed. The interactive verification tool KIV is the basis for this proof support. With this proof support the FTA condition can be verified over statechart specifications. A special feature of this statechart calculus is, that it allows the use of algebraically specified data types in statechart specifications, even infinite data types. The work ends with an application methodology for formal FTA and special tool suppport. It is possible to define fault trees over statechart specifications within KIV and generate the verification conditions for formal fault trees. These verification conditions can be proven with the developed statechart calculus. Therewith, a complete methodical and tool supported environment for formal fault tree analysis was developed.…