Software als Erfolgsgarant bei der Mars-Erkundung (und anderswo)

Die Februar-Ausgabe der Communications of the ACM (kurz CACM) enthält einen Beitrag von Gerard Holzmann mit den Titel ‚Mars Code‘. Er bekräftigt die Aussage, die ich in einem früheren Blog-Eintrag zitierte, dass nämlich Software-Entwicklung überschaubar ist, sofern die Ziele verstanden und die zu verwendende Technologie unter Kontrolle ist. Sie muss kein Abenteuer sein. Dass sie schwierig sein kann, und auch einiger Sorgfalt bedarf, bestreitet niemand. Meine Aussage bezog sich auf meine Erfahrungen aus den 1960er Jahren. Holzmanns Artikel beschreibt Erfahrungen mit dem Projekt, das den Rover Curiosity im August 2012 auf den Planeten Mars brachte.

In manchen Zirkeln gehörte das Jammern über die Software-Krise seit Jahrzehnten quasi zum guten Ton. Unzählige Fachartikel und viele Diplomarbeiten nehmen darauf Bezug. Ich hatte immer den Verdacht, dass hinter dem Jammern mitunter der Wunsch nach Forschungsgeldern stand. Da ich diese Gelder lieber bei der Software als bei der Hardware sah, hielt ich früher meine Meinung zurück. Ganz offensichtlich ignorierten die meisten dieser Autoren die gute Arbeit, die von vielen professionell arbeitenden Praktikern tagein tagaus gemacht wird. Sie selbst benutzen für ihre tägliche Arbeit Software, die angeblich unzumutbar ist. Sie machen dabei meist keinen Unterschied zwischen seriösen Produkten einerseits und amateurhaften Adhoc-Werkzeugen andererseits. Zweifellos ist in den Anforderungen an Software-Qualität ein weites Spektrum durchaus vertretbar. Nicht jedermann braucht dasselbe.

An der Spitze bezüglich Qualität und Zuverlässigkeit liegt eindeutig diejenige Software, die in lebenskritischen Geräten und Anwendungen verwandt wird. Medizinische Geräte gehören dazu, aber auch Aufzüge, Autos, Bahnen und Flugzeuge. Ich selbst habe wiederholt auf die amerikanische Raumfahrt hingewiesen. Was von dort bezüglich der Entwicklungsmethoden und der Ergebnisse in der Fachwelt berichtet wurde, ist in der Tat beeindruckend. Ich habe zuletzt auf diese Kollegen und ihre Methoden im Jahre 2010 in dem gemeinsam mit Rul Gunzenhäuser verfassten Buch ‚Schuld sind die Computer‘ (auf Seite 22) verwiesen.

Ein knochenharter Weg, der zu verlässlichen Ergebnissen [bezüglich Software-Qualität] führt, ist schon lange bekannt. Man korrigiert nicht nur die gefundenen Fehler, sondern sucht anschließend nach ähnlichen Fehlern sowie nach den gemeinsamen Ursachen. … Will man die Wiederholung eines Fehlertyps vermeiden, so muss man denjenigen Teil des Prozesses verbessern, der für die Entstehung dieses Fehlers verantwortlich ist. Dies ist zwar sofort einleuchtend, verlangt aber in der Praxis enorme zusätzliche Anstrengungen. Die amerikanische Raumfahrtindustrie, die diese Methode entwickelt hat und auch anwendet, ist bisher von ernsten Software-Problemen weitgehend verschont geblieben.

Was Holzmann berichtet, baut auf der im Zitat erwähnten Tradition der NASA auf und führt fort, was zur Zeit der Mondflüge entstand. In diesem Falle handelt es sich um das Jet Propulsion Laboratory (JPL) in Pasadena, CA.

Automatische Code-Analyse

Wie Holzmann berichtet, stehen heute sehr leistungsfähige Werkzeuge für die Code-Analyse von mehreren Lieferanten zur Verfügung. Hier scheint die Entwicklung in den letzten Jahrzehnten enorme Fortschritte gemacht zu haben. Natürlich gibt es Werkzeuge vor allem für die Sprachen, die Relevanz im Markt haben, also C, C++ und Java, und nicht für jede Spielzeugsprache, die von einem Lehrstuhl in Mittweida oder Honolulu gerade propagiert wird. Offensichtlich hat sich ein separater Markt entwickelt, unabhängig von den Compilern. Bei den C-Compilern gibt es etwa 30 Produkte, vorwiegend aus der Open-Source-Gemeinde.

Das Überraschende (für Holzmann) war, dass unterschiedliche Analyse-Werkzeuge unterschiedliche Fehler aufdecken. Als Konsequenz hat man nicht ein Werkzeug eingesetzt, sondern alle verfügbaren. Es macht diesen Programmen nichts aus, hundert mal denselben Fehler zu berichten. Kein Mensch würde dies machen. Gerade hier erfüllt sich eine Hoffnung oder Vision (ein Wort, das ich ansonsten vermeide), die ich einst hatte, dass nämlich Rechner dazu benutzt werden könnten, um die wachsende Komplexität von Software in den Griff zu bekommen. Einige der maschinell überprüften Eigenschaften des Codes, die im Bericht erwähnt werden, will ich deshalb angegeben:

• Keine compiler-abhängigen Spracherweiterungen, keine Fehlermeldungen oder Warnungen des Compilers oder der statischen Analyse-Werkzeuge.
• Ausführbarkeit in eingebetteter Systemumgebung gesichert; d.h. alle Schleifen mit statisch verifizierbarer Iterationszahl; alle Feld- und Array-Grenzen statisch überprüfbar; keine Division durch Null zugelassen.
• Dichte von Zusicherungen (% Anteil des Codes) erreicht eine Vorgabe.
• Keine Verwendung von Pointers, indirekter Adressierung, und dgl.
• Einhaltung aller MISRA-C-Regeln aus der Automobil-Industrie (z. B. kein Gleichheitsvergleich bei Gleitkommazahlen, kein goto, keine Rekursion)

Die MISRA (Abk. für Motor Industry Software Reliability Associatian) hat allein für die Sprache C über 100 Regeln festgelegt, die beachtet werden müssen, sollte diese Sprache in sicherheitskritischen Anwendungen benutzt werden. Da keine andere Programmiersprache eine vergleichbare Aufmerksamkeit erfahren hat, kann niemand behaupten, sie seien weniger gefährlich. Auch Unterschiede im Codierungsstil können mittels Strukturierungs-Werkzeugen ausgeglichen werden.

Entwurfs- und Code-Inspektionen

Wer die Diskussionen der 1960er Jahre in Erinnerung hat, weiß, welchen Stellenwert Inspektionen seither im Software-Entwicklungsprozess bekommen haben. Ich benutze das Wort Inspektionen als zusammenfassenden Begriff für Reviews, Walk-Throughs und dergleichen. Manche Kollegen glaubten fast, dass Inspektionen das Testen von Programmen ersetzen könnten. Zwei Regeln oder Grundsätze haben sich seither durchgesetzt: (1) Man inspiziert alle Arbeitsergebnisse so früh wie möglich, um die Lebensdauer eines Fehlers zu minimieren, (2) Man inspiziert jedes Arbeitsergebnis gezielt nach den Fehlerarten suchend, die erfahrungsgemäß zu erwarten sind, also mithilfe von empirisch gewonnenen Checklisten. Gerade der zweite Grundsatz hat bei der amerikanischen Raumfahrt-Software eine lange Tradition.

Durch Analyse-Werkzeuge wird die hohe Zeit- und Kostenbelastung, die früher durch Inspektionen entstand, erheblich reduziert. Dass gilt insbesondere bei Systemen, die mehrere Millionen Programmzeilen umfassen. Die Inspektionen können sich daher auf Dinge konzentrieren, die der Mensch besser als die Maschine machen kann. Das betrifft grundsätzlich das Aufspüren aller Entwurfsfehler, die ja bekanntlich oft katastrophale Folgen für ein Projekt haben können. Aber auch bestimmte Arten von   Implementierungsfehlern können durch Testen nicht gefunden werden. Viele Entwurfsfehler kann nur ein Fachexperte finden.

Wem die hier zur Anwendung gelangten Erfahrungen mit sprachabhängigen Fehlern schon etwas umfangreich erscheinen mag, der sollte bedenken, dass die Verantwortung eines Informatikers ja nicht nur aus der Beherrschung einer einzelnen Programmiersprache besteht. Auch die Planung, der Einsatz und die fehlerfreie Nutzung von Betriebssystemen, Datenverwaltungs- und Bildverarbeitungs-Software fallen in sein Ressort. Sich einzubilden, dass er auch noch die Kompetenz hätte für alle Anwendungsdomänen oder Fachdisziplinen, die in einem solchen Projekt mitwirken, davor muss er sich allerdings hüten. Es gehören dazu die Flugsteuerung im Gravitationsfeld mehrerer Körper, das Lenken autonom sich bewegender Fahrzeuge, die Erfassung und Auswertung von Telemetrie-Daten, die Messung und Prüfung von Temperatur-, Schwere-, Strahlungsdaten, und anderes mehr. Für alle diese Teilgebiete existieren empirische Daten über Anforderungs-, Entwurfs-, Implementierungs- und Testfehler, die von hochqualifizierten Spezialisten oder früheren Kollegen begangen wurden, bzw. ihnen unterliefen. Der Informatiker kann sich darum bemühen sicherzustellen, dass keine Brüche und Lücken auftreten, also keine Differenzen in den Maßeinheiten sich einschleichen, keine unverträglichen Versionen der entsprechenden Module eingespielt werden, usw. Er kann auch dafür sorgen, dass der Partikularismus der Experten sich in Grenzen hält.

Nicht nur für die Informatik auch für die andern Fachdisziplinen existieren empirische Untersuchungen, in denen die in vorausgegangenen oder ähnlichen Projekten aufgetretenen Fehler berichtet und analysiert werden. Holzmann ist der Ansicht, dass es für jemanden, der auf einem dieser Gebiete arbeitet, nicht schwer ist, an diese Daten zu gelangen. Aus Fehlern kann auf Fehlerursachen (engl. root causes) geschlossen werden. Das ergibt die Checklisten für alle späteren Inspektionen. Die Bezeichnung empirisches Software Engineering beschreibt diese Vorgehensweise.

Software-Redundanz

Dass man die Zuverlässigkeit von Hardware durch ihre Verdopplung erhöhen kann, ist ein allgemein bekanntes Prinzip. Software einfach zu verdoppeln dagegen ist unsinnig. Wenn sie Fehler enthält, werden diese auch dupliziert. Nur für die kritischste Phase des Projekts, die wenigen Minuten der Landung des Rovers, hatte man außer der Hardware auch die Software redundant ausgelegt. In einer zweiten Zentraleinheit befand sich eine zweite Implementierung derselben Funktionalität. Damit ein fliegender Wechsel von der einen Implementierung auf die andere möglich war, wurden beide Programme gestartet und synchron ausgeführt (engl. hot standby). Diese Implementierung derselben Funktion erhielt die Bezeichnung ‚Zweite Chance‘ (engl. second chance).

Eine zweite Form von Redundanz bestand darin, dass gewisse Teile des Codes mit Zusicherungen (engl. assertions) erweitert waren. Das sind Zustandsbedingungen, welche die Variablen erfüllen müssen, während der Code ausgeführt wird. Sehr oft werden solche Bedingungen nur zur Verifikation, also in der Entwicklungsphase, benutzt. Indem sie während des Betriebs laufend ausgewertet werden, kann festgestellt werden, ob eine unerwartete Situation eingetreten ist, die ein Umschalten auf die alternative Software erfordert.

Da ich die fachliche Diskussion der letzten Jahrzehnte um die formale Verifikation verfolgt habe, freut es mich sehr, dass zumindest diese Verwendung der einst so hochgelobten Technik übrig geblieben ist. Etwa 2-5 % des Codes wurden mit Zusicherungen versehen. Das entspricht nicht ganz den Erwartungen, die wir nach Tony Hoares Einführung der Methode in den 1970er Jahren mit ihr verbanden.

Model Checking

Das Model Checking ist ein aus der mathematischen Informatik stammendes Verfahren, das es erlaubt, durch eine Art von automatischem Durchspielen aller Fälle festzustellen, ob ein Programm die durch eine bestimmte formale Spezifikation beschriebene Eigenschaft erfüllt.

Benutzt wurde es im Mars-Rover-Projekt, um festzustellen, ob parallel ablaufende Routinen unter keinem denkbaren Szenarium unbeabsichtigte Wettlaufsituationen (engl. race conditions) verursachen. Da diese Tests völlig automatisch ablaufen, konnten sie leicht wiederholt werden, um sicherzugehen, dass durch Code-Änderungen keine neuen Fehler eingeführt wurden. Das bestätigt wiederum meine immer vertretene Auffassung, dass der Aufwand für mathematisch anspruchsvolle Verfahren sich umso eher lohnt, je mehr sie automatisiert werden können.

Sonstige Maßnahmen

Nur am Rande erwähnt sind in dem Artikel viele andere Maßnahmen, von denen man hoffen kann, dass sie längst Allgemeingut der Branche geworden sind, so dass jeder Neuling sie in der Schule lernt. Dazu gehören gute Software-Architekturen basierend auf

‘clean separation of concerns, data hiding, modularity, well-defined interfaces, and strong fault-protection mechanisms.’ (Die Übersetzung erspar ich mir).

Über Testen spricht der Artikel nicht. Ich gehe davon aus, dass man nicht den Fehler machte, Testen durch Analysen und Inspektionen zu ersetzen. Auch Leistungsmessungen werden nicht erwähnt. Sie fielen sicher nicht unter den Tisch, obwohl die Software nur einen einzigen Nutzer hat. Interessant ist auch, was nicht erwähnt wird. Die ganze objekt-orientierte Technik scheint keine Rolle zu spielen.

Reflexionen eines Außenstehenden

Während der Autor damit argumentiert, dass bei diesem Projekt außer sehr hohen Investitionen auch der Ruf der NASA auf dem Spiel standen, fallen mir noch weitere Themen ein, über die nachzudenken sich lohnt.

Die unbemannte wie die bemannte Raumfahrt stellen außergewöhnliche technische und menschliche Leistungen dar. Sie würden selbst einem extraterrestrischen Besucher Respekt abverlangen. Wir Erdlinge haben es den amerikanischen Bemühungen zu verdanken, dass wir heute auf unser Sonnensystem von Außen blicken können (dank Voyager 1 und 2) und dass wir laufend für uns neue ferne Galaxien entdecken (dank der Hubble-Sonde).

Die erzielten Erfolge machen Mut, eventuell auch andere Fragen und Probleme in Angriff zu nehmen, die Menschen bewegen (Stichworte Ernährung, Seuchen, Umwelt, Klima). Es muss zuerst der Wille zur gemeinsamen Leistung entstehen. Bei der Durchführung des entsprechenden Projekts muss mit Nüchternheit und Entschlossenheit vorgegangen werden. Es wird erforderlich sein, auf den Leistungen vieler aufzubauen, nicht nur auf den Schultern von einigen Riesen zu stehen. Dabei lernen wir vor allem durch die Fehler und das Versagen derjenigen, die sich an ähnlichen Aufgaben versucht haben. Zu Lehrmeistern können unsere Mitbewerber werden, unsere Kollegen, unsere Freunde oder wir selbst.