Marslander Phoenix geland dankzij goed geteste software

Zondag 25 mei landde de Amerikaanse robotverkenner Phoenix na een reis van bijna tien maanden op Mars. De software van de Phoenix is erg grondig gecontroleerd. Hoe essentieel dat is, bleek in december 1999. De toenmalige Marslander zette zijn remmotoren uit voordat het oppervlak van Mars bereikt was en crashte.

Zondag 25 mei landde de Amerikaanse robotverkenner Phoenix na een reis van bijna tien maanden op Mars. De software van de Phoenix is erg grondig gecontroleerd. Hoe essentieel 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.”

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.

Gerard Holzmann deed zijn uitspraken aan onze collega’s van Computable na afloop van een lezing die hij vrijdag 23 mei gaf ter ere van het vijfentwintig bestaan van de SEN2 groep van het Nederlandse Centrum voor Wiskunde en Informatica (CWI). Die groep houdt zich sinds 1982 bezig met het ontwikkelen van algebraïsche technieken voor de specificatie en verificatie van softwaresystemen.

In samenwerking met Computable

Fout opgemerkt of meer nieuws? Meld het hier

Partner Content