Un logiciel parfaitement testé à la base de l’atterrissage réussi de Phoenix Marslander

Ce dimanche 25 mai, la sonde américaine Phoenix s’est posée sans problème sur Mars après un voyage de quasiment dix mois. Le logiciel embarqué avait été dûment contrôlé. En décembre 1999, l’on avait en effet observé combien c’est essentiel. La sonde de l’époque avait désactivé ses moteurs de freinage avant d’avoir atteint la surface de Mars et s’était crashée.

Ce dimanche 25 mai, la sonde américaine Phoenix s’est posée sans problème sur Mars après un voyage de quasiment dix mois. Le logiciel embarqué avait été dûment contrôlé. En décembre 1999, l’on avait en effet observé combien c’est essentiel. La sonde de l’époque avait désactivé ses moteurs de freinage avant d’avoir atteint la surface de Mars et s’était crashée.

La fiabilité du logiciel de la sonde Phoenix a été contrôlée dans le détail par le Jet Propulsion Laboratory (JPL) de la Nasa. Gerard Holzmann du JPL: “Lockheed a construit la sonde et y a embarqué le logiciel de commande. Nous avons analysé le code de Lockheed et y avons certes trouvé quelques bugs, mais rien de spectaculaire: il s’agit du même type de défaut de programmation qu’on trouve dans chaque espèce de code, comme l’utilisation d’une variable non initialisée. Le standard industriel, c’est que du point de vue statistique, l’on rencontre d’1 à 10 erreurs de ce genre par tranche de 1.000 lignes de code.”

On a déjà plusieurs fois constaté combien il est important de tester le logiciel de commande des vaisseaux spatiaux. On l’a ainsi observé douloureusement en décembre 1999, lorsque la sonde de l’époque avait désactivé ses rétro-moteurs avant d’atteindre la surface de Mars. Cette décision fatale fut probablement prise, à en croire la NASA, parce qu’un capteur sur l’un des trois pieds d’atterrissage avait été tellement sollicité lors de la descente que le logiciel en était venu à conclure que la sonde avait déjà atterri.

Gerard Holzmann a fait ses déclarations à nos collègues de Computable au terme d’une conférence qu’il a tenue le vendredi 23 mai en l’honneur des 25 ans d’existence du groupe SEN2 du ‘Centrum voor Wiskunde en Informatica’ (CWI) néerlandais. Ce groupe est depuis 1982 en charge du développement de techniques algébriques pour la spécification et la vérification des systèmes logiciels.

En collaboration avec Computable