http://www.siam.org/siamnews/general/ariane.htm

Einige zusätzliche Details:

• Der Absturz wurde verursacht durch den gleichzeitigten Ausfall zweier identer, redundanter Systeme zur Messung von räumliche Lage und Beschleunigung (SRI).
• Das übergeordnete System registrierte das Versagen beider Systeme und löste die Selbstzerstörung aus.
• Der Ausfall der SRIs wurde verursacht durch einen Überlauf bei der Umwandlung eines Messwertes von 64-Bit-Float in 16-Bit-Int.
• Die ausgelöste Overflow-Exception wurde nirgendwo abgefangen und führte zum Ausfall der Systeme. Andere Messwertumwandlungen waren gegen solche Überlauf-Probleme geschützt.
• Nicht ganz. Aus dem obengenannten Bericht: "The supplier of the SRI followed the specifications given to it, which stipulated that in the event of any detected exception the processor was to be stopped."

Aus irgendwelchen Gründen wurde angenommen, daß die Software fehlerfrei wäre und deshalb keine Exception auftreten würde, außer wenn ein Hardwaredefekt vorliegt. Diese Annahme der Korrektheit war der eigentliche Fehler.

• Die Software war von der Ariane 4 Rakete übernommen worden, bei der die Messwerte in einem geringeren Wertebereich anfielen.
• Der Rechenwert, der den Absturz auslöste, wurde zu dem Zeitpunkt gar nicht mehr benötigt. Gemessen wurde noch, weil dies bei der Ariane 4 zu diesem Zeitpunkt noch notwendig war.

Was hätte den Absturz eventuell vermeiden können (rein spekulativ -- HelmutLeitner):

• Wenn der Messzeitraum an die Erfordernisse de Ariane 5 angepasst wäre, dann wäre die Messung mit dem Start beendet worden (Es wäre plausibel, diesen Zeitraum zu überprüfen und anzupassen)
• Wenn der Programmierer der Software für die Ariane 4 generell alle Overflow-Exceptions gleich behandelt hätte (wäre plausibel, das zu tun) obwohl er wußte, dass es in seinem System zu solchen Werten nicht kommen würde.
• Wenn es ein Kontrollverfahren gegeben hätte, bei dem sichergestellt worden wäre, dass alle Exceptions ordnungsgenmäß abgefangen werden (wäre plausibel, so etwas zu haben)
• Wenn die Softwareentwickler beim Übergang auf die Ariane 5 erkannt hätten, dass es in diesem Bereich zu einem Overflow-Problem kommen könnte (sehr unplausibel, dass etwas so ins Detail mit so großer Aufmerksamkeit geprüft werden kann).
• Wenn eine geeignete SoftwareQualitätssicherung gegriffen hätte.

Der Code wurde ursprünglich für die Ariane 4 geschrieben. Für deren Flugbahn hatte der Programmierer wohl bewiesen, dass kein Overflow auftreten kann bzw. der Overflow auf ein defektes System hinweisen würde. Seine Fehlerbehandlung war also absolut korrekt; kein noch so hoher Aufwand an formaler Überprüfung und systematischer Behandlung von Exceptions hätte daran etwas ändern können. Eine Ariane 4, die diesen Rechenfehler produzierte, hätte korrekterweise gesprengt werden müssen, auch wenn ein spezieller Handler die Exception abgefangen hätte, hätte er daraufhin explizit die Sprengung auslösen müssen.

Der einzige Weg, das Problem bei der Umstellung auf die Ariane 5 zu erkennen, hätte darin bestanden, den geführten Beweis zu überprüfen. Ich nehme stark an, das wurde eingespart; bei diesem Projekt gab es bestimmt genug Papierdoku, die zur Beweisüberprüfung zur Verfügung gestanden hätte.

Wäre natürlich toll, wenn man die Beweise computerverständlich führen könnte, mit so einem automatischen Beweisprüfer. Der müsste den Beweis dann unter veränderten Ausgangsbedingungen leicht erneut prüfen können. Aber so ein formaler Beweis ist sicher enorm aufwändig. Weiß eigentlich jemand, ob man den Ausfall durch eine Simulation hätte vorher sehen können? -- HenningThielemann

Es würde reichen, wenn die Assertion (dass die Bahnabweichung klein genug ist) formalisiert würde. Wenn der Beweis nicht compilerverständlich geführt werden kann, muss eben die Assertion explizit ins System hineingesteckt werden; damit gibt es eine prominente Stelle, an der die impliziten, manuell zu checkenden Annahmen zusammenlaufen. Solche Systeme lassen sich sogar im Typchecker eines Compilers integrieren, obwohl das alles noch etwas experimentiell ist (vgl. SpracheCayenne).

Unanbhängig davon fragt man sich, warum der Fehler bei keiner Simulation auftrat. Man muss ja fast annehmen, dass keine Simulation stattgefunden hat.

Critique of "Put it in the contract: The lessons of Ariane" by Ken Garlington