Vorsicht ist besser als Bananen-Software

9. Oktober 2013, 13:59
27 Postings

Softwarefehler können in Raumfahrt, Medizin oder bei der U-Bahn-Steuerung schwere Folgen haben - Um Bugs von vornherein möglichst auszuschließen, empfehlen Forscher die Verwendung "rigoroser Methoden"

Software, die vom Entwickler an den Verwender weitergegeben wird, ohne sie davor ausreichend zu testen, wird in den IT-Abteilungen gerne "Bananen-Software" genannt. Auf das Leiden durch allerlei Bugs folgen Beschwerden, Patches und Updates - Bananen-Software "reift" erst beim Kunden.

Was im Fall eines neuen Buchhaltungsprogramms ärgerlich sein mag, kann bei Anwendungen in der Medizin, in der Raum- und Luftfahrt oder im öffentlichen Verkehr gefährlich sein. Berühmt geworden ist der Softwarefehler, der den Erstflug der europäischen Trägerrakete Ariane 5 im Jahr 1996 zum Desaster werden ließ: Knapp 40 Sekunden nach dem Start explodierte der Raumfrachter samt den geladenen Satelliten.

Ein Modul, das für die Vorgängerin Ariane 4 gut funktionierte, wurde ungeprüft übernommen und führte unter den veränderten Bedingungen der neuen Rakete - sie beschleunigte schneller - zu einem Fehler, der eine Kettenreaktion auslöste.

Über die vergangenen Jahrzehnte hat sich beim Erstellen sicherheitskritischer Anwendungen eine Herangehensweise etabliert, die Fehler weitgehend ausschließen soll: Bei "formalen Methoden" oder "rigorosen Methoden", wie sie Klaus-Dieter Schewe, Forscher am Software Competence Center Hagenberg (SCCH), nennt, liegt der Schwerpunkt auf der Konzeptualisierung der Software. "Der größte Teil der Fehler wird am Anfang gemacht", erklärt Schewe. "Weil der Entwickler nicht genau weiß, was der Anwender genau will und warum er das will." Auf die Validierung, den nachprüfbaren Weg zum Ziel, werde besonderer Wert gelegt. Es muss dokumentiert sein, dass sich die Anforderungen in den Spezifikationen wiederfinden.

In der Entwicklung der Software werden diese Spezifikationen in einer logisch nachvollziehbaren, formalen Sprache notiert, einer Metasprache, die nach und nach mit Programmteilen "systematisch angereichert" werden soll. Bestimmte Eigenschaften, Fehlerfreiheit in manchen Aspekten, könne mit Tools oder, so Schewe, zur Not mit Papier und Bleistift mathematisch bewiesen werden. "Das Testen von Software ist immer ein unvollständiger Prozess. Die Verifikation im Rahmen der rigorosen Methoden ist nicht notwendigerweise unvollständig - ein entscheidender Punkt, warum sie propagiert werden", erklärt der Forscher.

Ungeduld macht Probleme

Auf diese Art soll ein System erzeugt werden, in dem möglichst einfach der tatsächliche Programmcode erzeugt werden kann. Beim Programmieren selbst entstünden die wenigsten Fehler, erklärt Schewe. Im Vorfeld müsse man aber ausschließen, dass es keine Zweideutigkeiten gibt, die der Programmierer falsch interpretieren kann. Rigorose Methoden zielen also auch darauf ab, dass der Aufwand für das Testen minimiert wird. Allerdings befriedigen sie nicht die Wünsche von Anwendern und Entwicklern, die möglichst schnell etwas vom werdenden Produkt sehen wollen.

Eine Paradeanwendung rigoroser Methoden, auf die oft verwiesen wird, ist die Software für die automatische Steuerung führerloser Züge der Pariser Métro. Insgesamt sei dort der Entwicklungsaufwand bis zum laufenden System im Vergleich zum konventionellen Programmieren relativ gering gewesen, sagt Schewe. Fehler sei bisher keiner aufgetreten. Die aufsehenerregenden Probleme, wie sie zuletzt im Online-Banking einer Bank in Österreich aufgetreten sind, seien, so Schewe, wohl ohne den Einsatz rigoroser Methoden entstanden. "Banken sind bei Softwareentwicklung sehr konservativ."

Dabei ist gerade in Österreich eine frühe Variante der rigosrosen Methoden entwickelt worden. Der Däne Dines Björner, der im Wiener IBM Labor arbeitete, entwickelte in den 1970er-Jahren die sogenannte Vienna Development Method (VDM), deren Nachfolger noch heute existieren. Daneben gibt es populärere Systeme wie Event-B, die auch für die französischen U-Bahnen verwendet wird, oder Abstract State Machine (ASM). Sie haben jeweils eigene "Werkzeugkästen", Software-Tools, um Code zu erstellen oder zu interpretieren, die oft an Unis entworfen und weiterentwickelt werden. Darin liege laut Schewe auch ein Problem: Werkzeuge kommen und gehen - was nicht gerade im Sinne eines langfristig verlässlichen Verfahrens ist.

Mit Event-B und ASM beschäftigt sich auch der Hagenberger Forscher. Seine Gruppe wendet die rigorosen Methoden nicht nur an, sondern versucht sie auch für weitere Zwecke, etwa zeitgemäße, stark verteilte Softwaresysteme zu adaptieren. Wenn etwa in einer Produktionsstraße eine Reihe von Robotern mit gleicher Software läuft und einer ausfällt, sollen die anderen den Fehler erkennen und die Aufgabe des kaputten Kollegen unter sich aufteilen. Auch derartige komplexe Anwendungen sollen künftig mit rigorosen Methoden erstellt werden können. (Alois Pumhösel, DER STANDARD, 9.10.2013)

  • Software, die für flüssigen U-Bahn-Verkehr sorgt, muss verlässlich sein. Formale Methoden helfen bei ihrer Entwicklung.
    foto: standard/corn

    Software, die für flüssigen U-Bahn-Verkehr sorgt, muss verlässlich sein. Formale Methoden helfen bei ihrer Entwicklung.

Share if you care.