Formale Methoden

Für sicherheitskritische Systeme

In der Medizin, im Transportwesen (vollautomatische Züge, Raumfahrt) oder in der Energieproduktion (Kernkraftwerke) können Softwarefehler schwerwiegende Folgen haben.  Verwendet man formale Methoden, dann könnten solche Bugs im Vorhinein vermieden  werden. Während die Zuverlässigkeit von einfachen Maschinen sich durch Prüfungen und Tests ermitteln lässt, ist die Beurteilung der Sicherheit von softwaregesteuerten Maschinen mit komplexem Verhalten äußerst schwierig. Hier können Tests nur das Vorhandensein von Fehlern zeigen, nicht aber deren Abwesenheit beweisen. Fehler in Softwarekomponenten können zu den verschiedensten Zeitpunkten im Verlauf des Entwicklungsprozesses entstehen - angefangen bei einer inadäquaten Anforderungsspezifikation  über Fehler im Entwurf bis hin zu Implementierungs- und Integrationsfehlern, alle stellen eine potentielle Gefahr im späteren Betrieb des Systems dar. Es gibt  daher verschiedene Ansätze, um die Zuverlässigkeit von Software zu erhöhen.

Im Interview erzählt Frau Dr. Christine Natschläger warum formale Methoden in Zukunft immer bedeutsamer werden und warum sie aber immer noch ein Nischendasein führen.

Dr. Christine Natschläger moderierte die Veranstaltung "Systems Engineering für Industrie 4.0"

Was sind formale Methoden?

Bei der Entwicklung sicherheitskritischer Software hat sich eine Herangehensweise etabliert, die Fehler von Anbeginn  vermeiden soll. Bei den formalen Methoden liegt der Schwerpunkt auf der Konzeptualisierung der Software. Sie bauen auf mathematischer Modellierung und formaler Logik auf und werden verwendet, um die Software zu spezifizieren und zu prüfen. Mit formalen Methoden kann man von einem mathematischen Modell ausgehend durch die logische Analyse die Eigenschaften eines Systems voraussagen.  Es kann festgestellt werden, ob eine Systembeschreibung (Spezifikation) in sich konsistent ist, ob bestimmte Eigenschaften garantiert werden können und ob die Anforderungen richtig entworfen und implementiert wurden. Außerdem kann die Spezifikation für die Simulation/Animation, zur Codegenerierung, zur Testgenerierung und zur Testauswertung benutzt werden. 

In welchen Bereichen können formale Methoden besonders gut eingesetzt werden?

Zum Beispiel Event-B und ASMs (Abstract State Machines) werden verwendet, um sicherheitskritische Systeme (ein Beispiel wäre die Pariser RER Bahn, die vollautomatisch fährt und noch nie einen Fehler hatte) und auch stark verteilte Softwaresysteme zu entwickeln.  Wenn etwa in einer Produktionsstraße mit einer Reihe von Robotern mit gleicher Software ein Roboter  ausfällt, so sollen die anderen Roboter den Fehler erkennen und die Aufgaben des defekten Roboters unter sich aufteilen. Für derartig komplexe Anwendungen eignen sich formale Methoden.
Es gibt aber auch andere Anwendungsbeispiele, wie zum Beispiel Dialysegeräte, Herzschrittmacher oder Flugzeug-Komponenten. All diese Systeme sind repräsentativ für sicherheitskritische, eingebettete System und die erste Herausforderung besteht in der Modellierung der Systeme. Die zweite Herausforderung ist dann der Nachweis der Einhaltung der Sicherheitsanforderungen und der richtigen Funktion unter Rücksichtnahme auf das physische Verhalten der Geräte.

Wie unterscheidet sich die Entwicklung mit formalen Methoden von der herkömmlichen Softwareentwicklung?

Es verschiebt sich einiges an Aufwand und Zeitverbrauch im Projekt: Es wird mehr Sorgfalt in die Anforderungsanalyse, die Spezifikation und das Grob-Design gesteckt; dieser Mehraufwand kann aber dadurch wieder hereingeholt oder sogar überkompensiert werden, dass während der Implementierung wesentlich weniger Spezifikations- und Designfehler mühsam identifiziert und behoben werden müssen und auch die Testphase schneller durchlaufen werden kann. Bei der Auswahl geeigneter, modell-basierter Methoden kann das für Spezifikation, Validierung und Verifikation erstellte Modell auch zur Unterstützung von Implementierung, Test-Suite-Erstellung, Dokumentation und schließlich auch Wartung wiederverwendet werden.

Welche Eigenschaften hat die Entwicklung mit formalen Methoden?

  • Der Entwickler muss das System besser kennen!
    Der mit der Spezifikation beauftragte Systementwickler ist gezwungen, sich mehr Gedanken über das zu entwickelnde System zu machen und er muss es im Detail verstehen. Sein Zeitaufwand wird wesentlich höher sein als sonst. Da er jedoch genauer darüber nachdenkt, was zu implementieren ist, werden die folgenden Schritte (Entwurf, Implementierung, Integration) weniger experimenteller Natur sein, weniger Fehler verursachen und Zeit einsparen.
  • Validierung
    Mit formalen Methoden kann das System noch vor der Implementierung durch Animation (Simulation) validiert werden.
  • Verifikation
    Durch Verifikation wird überprüft, ob die Spezifikation in sich konsistent (frei von Widersprüchen) ist, ob bestimmte Eigenschaften (z.B. Sicherheitsanforderungen) garantiert werden können und ob die Anforderungen richtig umgesetzt wurden.
  • Mensch-zu-Mensch-Kommunikation
    Mit einer formalen Spezifikation liegen präzise Aussagen (ohne Zweideutigkeiten) über das gewünschte Verhalten vor. Formalisierung unterstützt damit die eindeutige Kommunikation unter den Entwicklern.
  • Automatische Code Generierung
    Manche (operationale) Formalismen erlauben bei einem genügend hohen Detaillierungsgrad eine automatische Code-Generierung aus der Anforderungsspezifikation. Allerdings muss der generierte Code meist noch nachgebessert werden.

Können formale Methoden alle Softwarefehler vermeiden?

Von allen Fehlern, die bei der Inbetriebnahme und im Betrieb gefunden werden, kommen die meisten und die teuersten aus der Anforderungsspezifikation. Die Fehler aus der Implementierung sind seltener und oft  einfacher (billiger) zu korrigieren. Die Spezifikationsfehler können sich durch die ganze Implementierung ziehen und große Änderungen nötig machen. Die schwerwiegendsten Fehler bestehen darin, dass nicht das gewünschte Verhalten spezifiziert wurde. Dies kann durch Validierung im ersten Schritt geprüft werden. Der nächst-schwerwiegende Fehler besteht darin, dass der Entwurf die Anforderungen nicht erfüllt.

Mit welchem Aufwand ist zu rechnen, wenn man formale Methoden einsetzt?

Der Aufwand bei der Verwendung von formalen Methoden ist bei der Anforderungsspezifikation relativ niedrig und die Anzahl der Fehler, die dabei gefunden werden können, verhältnismäßig hoch. Bei der Implementierung ist ihre Anwendung aufwendiger, und die Anzahl der Fehler, die sie aufdecken können, niedriger. Abhängig von den möglichen Fehlerkosten (fehlerhafte sicherheitskritische Systeme können Leben gefährden), kann aber auch in dieser Phase der Einsatz sinnvoll sein.

 

 

 

zurück