Advertisement

Informatik - Forschung und Entwicklung

, Volume 14, Issue 4, pp 193–202 | Cite as

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

  • Wolfgang Reif
Orignalbeiträge

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.

Schlüsselwörter: Softwaretechnik, Qualitätssicherung, Sichere und korrekte Systeme, Formale Methoden, Spezifikation, Verifikation, Maschinelles Beweisen 

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.

Key words: Software Engineering, quality assurance, correct and secure systems, formal methods, specification techniques, verification, mechanical theorem proving 
CR Subject Classification: D.2, D.2.4, F.3.1, F.4.1, I.2.2, K.6.4 

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

Copyright information

© Springer-Verlag Berlin Heidelberg 1999

Authors and Affiliations

  • Wolfgang Reif
    • 1
  1. 1.Universität Ulm, Abteilung Programmiermethodik, D-89069 Ulm (e-mail: reif@informatik.uni-ulm.de) Deutschland

Personalised recommendations