Zondag 25 mei landde de Amerikaanse robotverkenner Phoenix na een reis van bijna tien maanden op Mars. De software van de Phoenix is grondig gecontroleerd. Hoe nodig dat is bleek in december 1999. De toenmalige Marslander zette zijn remmotoren uit voordat het oppervlak van Mars bereikt was en crashte.
De software van robotverkenner Phoenix is door Nasa's Jet Propulsion Laboratory (JPL) uitgebreid op betrouwbaarheid gecontroleerd. Gerard Holzmann van het JPL: "Lockheed heeft het ruimtevaartuig gebouwd inclusief de bijbehorende besturingssoftware. We hebben de code van Lockheed geanalyseerd. Natuurlijk zijn daarbij fouten gevonden. Niets spectaculairs: het gaat om hetzelfde type programmeerdefecten dat je in elk type code vindt, zoals het gebruiken van een variabele die niet geïnitialiseerd is. De industriestandaard is dat je statistisch gezien tussen de 1 en 10 van dit soort fouten aantreft voor elke 1000 regels code."
Fatale crash in 1999
Hoe nodig het is om de besturingssoftware van ruimtevaartuigen te testen is al meermaals gebleken. Dat bleek bijvoorbeeld pijnlijk in december 1999, toen de toenmalige Marslander zijn remmotoren uitzette voordat het oppervlak van Mars bereikt was. Deze fatale beslissing werd volgens NASA waarschijnlijk genomen doordat een sensor op één van de drie landingspoten tijdens het afdalen zo op de proef werd gesteld dat de software concludeerde dat de Marslander al geland was.
Verificatie van softwaresystemen
Gerard Holzmann deed zijn uitspraken aan Computable na afloop van een lezing die hij vrijdag 23 mei bij het CWI gaf ter ere van het vijfentwintig bestaan van de SEN2 groep. Deze groep houdt zich sinds 1982 bezig met het ontwikkelen van algebraïsche technieken voor de specificatie en verificatie van softwaresystemen.
Gerard Holzmann
Gerard Holzmann promoveerde in 1979 als informaticus in Delft. Tussen 1980 en 2003 maakte hij binnen Bell Labs deel uit van de Computing Science Research groep, waarbinnen onder andere de programmeertalen C en C++ ontwikkeld werden. Holzmann werkte er tien jaar aan de SPIN model checker, een softwaretool voor het controleren van de betrouwbaarheid van gedistribueerde softwaresystemen. Hiervoor ontving hij in in 2002 de Software System Award van de Amerikaanse Association for Computing Machinery. Vanaf 2003 werkt Holzmann bij het Jet Propulsion Laboratory van NASA aan het verbeteren van de betrouwbaarheid van de software voor ruimtevaartuigen.
Phoenix
Phoenix gaat naar (resten van) leven zoeken in de ijslaag op de Noordpool van Mars. Een hitteschild moet de Marslander beschermen tijdens het afremmen in de atmosfeer. Als de Phoenix bijna zijn doel heeft bereikt werpt hij zijn parachute af en schakelt zijn remraketten in voor het laatste deel van de landing.
Hoogst interesant.
Hey dit is dezelfde geitenwollensokken figuur die zei dat Vista onbetrouwbaar was…..dat die marslander nog met software uit 1980 begreep, was zeker een ZX-80 speciaal voor dit project bewaard :-S