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.

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.

Die Autorin: Dr. Christine Natschläger hat ein Diplom in Software Engineering im Medizinbereich und einen Master in Information Engineering & -Management. Ihre Doktorarbeit verfasste Sie zu den Themen BPMN (und deontische Logik). Seit 2004 forscht sie am Software Competence Center Hagenberg in den Bereichen Business Process Modelling (mit formalen Definitionen) und Process Mining. Seit 2015 leitet sie den Forschungsschwerpunkt Rigorous Methods in Software Engineering.

Mehr Information: In einem jüngeren Beispiel über die erfolgreiche Einführung formaler Methoden berichten die Entwickler von Amazon Web Services und wie sie dadurch Software-Qualität und Produktivität verbessern konnten – siehe dazu: How Amazon Web Services Uses Formal Methods: http://cacm.acm.org/magazines/2015/4/184701-how-amazon-web-services-uses-formal-methods/abstract

Das Software Competence Center Hagenberg war auch Co-Organisator der ABZ 2016 – Die internationale Konferenz, bei der Entwickler und Anwender der wichtigsten modell-basierten formalen Methoden zusammen kommen: http://www.cdcc.faw.jku.at/ABZ2016/

Dieser Beitrag wurde unter IT-Management, Software veröffentlicht. Setze ein Lesezeichen auf den Permalink.

Schreibe einen Kommentar

Deine E-Mail-Adresse wird nicht veröffentlicht. Erforderliche Felder sind markiert *