Ces satellites s’appelent CubeSat. Il se trouve que leurs logiciels écrits en C, mais par de très bon développeur(se)s de la NASA, avec de grosses batteries de testes, sont actuellement en cours de conversion en Ada, et plus précisement en SPARK, un sous ensemble de Ada qui permet la démonstration formelle de programme Ada, c’est à dire que la validité des programmes envers leurs spécifications sont mathématiquement et logiquement démontré.
25% des logiciels C de CubeSat ont déjà été converti, et des erreurs dans les programmes initiaux en C ont été découvertes à cette occasion [1]. Le projet de conversion est actuellement mené par des étudiants. Il ne faut pas en être surpris(e), car s’agissant de validation formelle, ce n’est pas l’apriori de confiance ou d’expérience, mais la preuve formelle qui fait foi.
De nombreuses sondes spatiales, satellites et vaisseaux spatiaux, sont pilotés par des programmes Ada.
C’est ce qui les rend fiables, mais n’élimine cependant pas toute les causes d’erreurs. Un exemple malheureux est celui d’une sonde qui s’est écrasé sur Mars, je ne sais plus laquelle, parce que les ingénieurs avait confondu les unités SI et les unités de ces bougres d’andouilles d’anglo‑saxon qui n’ont toujours pas compris l’intérêt d’un système d’unité standard. Pfff, franchement, perdre une sonde sur Mars juste pour ne pas avoir voulu froisser la reine d’Angleterre, ctronul :mad:
[1]
comp.lang.ada — Ada advocacy — 2012-03-25 13:10
Peter C. Chapin a écrit> And some rumors says: There are still small teams of programmers
> doing backports of some of the NASA C/C++ SW to Ada again, and they
> are finding "intresting" bugs that are repored back to NASA again.
Those rumors might be pertaining to the CubeSat work we are doing at
Vermont Technical College. NASA is allowing us to use some navigation
software they developed. The software is written in C and, as C programs
go, is reasonably well done. We are working on converting it to SPARK...
a process that is ongoing. We have found a few "anomalies" so far---I'm
not sure I'd call them outright bugs---but we have only translated about
25% of the code and we are far from completing all the proofs.
Most of the programmers on this project are students and most of the
progress on it gets made during the summer.
Peter
Pour les sondes planétaires robotisées et les satellites, SPARK/Ada caytrolbien 🙂
