Formale Methoden für sicherheitskritische Software – Der KIV-Ansatz

Zusammenfassung.

Im Spektrum der qualitätssichernden Maßnahmen im Software-Entwurf gehören formale Spezifikations- und Verifikationsmethoden heute zweifellos zu den stärksten Waffen in puncto Fehlererkennung und Nachweis von Korrektheitseigenschaften. Mit zunehmender Wirtschaftlichkeit formaler Methoden und in Kombination mit klassischen Techniken der Qualitätssicherung ergeben sich dadurch neue, weitreichende Möglichkeiten. Die Wirksamkeit formaler Methoden beruht im wesentlichen auf der Mathematisierung von Teilen der Software-Entwicklung und dem damit verbundenen Zwang zur Präzision. Auf dieser Basis können Fehler entdeckt, Korrektheits- und Sicherheitseigenschaften nachgewiesen und die Auswirkungen von Systemänderungen formal analysiert werden. Diese Methoden eignen sich besonders für Anwendungen, an die traditionell höchste Zuverlässigkeits- und Qualitätsanforderungen gestellt werden. Dieser Artikel gibt einen Überblicküber verschiedene Einsatzmöglichkeiten formaler Spezifikations- und Verifikationsmethoden und stellt das KIV System vor, ein fortgeschrittenes Werkzeug zur Anwendung formaler Methoden. Am Beispiel von KIV wird der aktuelle Leistungsstand und die Wirtschaftlichkeit der Technologie erläutert.

Abstract.

In the field of Software Engineering methods for quality assurance, formal specification and verification are excellent techniques for rigorous error detection, and correctness proofs. With the increasing cost effectiveness of formal methods, the combination of both formal and classical quality assurance techniques may lead to a significant improvement of software quality. The effectiveness of formal methods basically is due to the mathematical modelling of parts of the software development, and the corresponding demand for precision imposed on the developer. Formal models allow for systematic error detection, correctness proofs, and rigorous analysis of system changes. Formal methods are appropriate for applications with very high reliability, and quality requirements. This article gives an overview of how and where to apply formal specification and verification methods. The current state of affairs is illustrated with KIV, an advanced support tool for formal methods.