DeepSpec : un projet logiciel qui permettra de développer des logiciels sans bogue ?

Une aventure du MIT et de quelques partenaires

DeepSpec est un projet logiciel financé par la National Science Foundation (NSF) à hauteur de dix millions de dollars et porté par le Massachusetts Institute of Technology, l’université de Pennsylvanie et l’université Yale. Le but du projet est de développer un système intégré d’outils permettant d’éliminer les bogues dans les systèmes logiciels complexes. Le projet se veut très ambitieux. En effet, les chercheurs autour du projet affirment que leur objectif au-delà de la recherche de base c’est de refaçonner l’industrie elle-même de sorte à fédérer les progrès que différents chercheurs ont eu à faire dans ce domaine. Un des objectifs est notamment de former la prochaine génération de développeurs et d’ingénieurs aux bonnes pratiques pouvant les mener vers l’objectif zéro bogue dans leurs programmes.

Le défi majeur pour ces chercheurs, d’après des membres de leur équipe, sera d’arriver à comprendre et à maitriser la complexité des matériels et logiciels modernes et de déterminer les facteurs importants intervenant quand deux composants logiciels sont mis ensemble pour faire une tâche définie. Un autre défi, pas des moindres, sera ensuite de faire une description précise du comportement des logiciels basés sur la logique formelle (raisonnement déductif, utilisation de syllogismes, mathématiques). Cela va permettre à terme aux ingénieurs non seulement de développer des logiciels sans bogue, mais aussi de vérifier la conformité de ces derniers à en croire les membres du projet.

Un tel projet requiert beaucoup de moyens financiers et un temps suffisamment long pour être mené à bien. C’est ce qu’a compris la NSF en acceptant de le financer. En effet, Jim Kurose qui est à la tête de la fondation a déclaré que : le programme DeepSpec « permet à la communauté de chercheurs en informatique de poursuivre l’étude de problèmes complexes en informatique sur une longue période ». Il ajoute que « cela permettra à ces chercheurs de faire des avancées non seulement pour les disciplines des sciences de l’ordinateur, mais aussi pour d’autres domaines.

Selon l’équipe de chercheurs, ce projet vient à son heure, dans un contexte où la majeure partie des techniciens dans l’industrie logicielle considèrent l’écriture de logiciel plus comme un art qu’une discipline scientifique. Cet aspect des choses fait notamment que les programmeurs, qui travaillent la plupart du temps sur des tâches isolées, ne se soucient pas de documenter et de codifier suffisamment leurs travaux pour que les autres puissent s’en servir comme base dans leur apprentissage. Les chercheurs autour du projet estiment que la faiblesse de la base institutionnelle de la connaissance a ralenti les progrès dans la recherche de solutions à ce qui peut être qualifié comme une énigme à savoir les comportements imprévisibles résultants de la mise ensemble de plusieurs programmes pour faire un travail donné. Andrew Appel, à la tête de l’équipe de chercheurs, déclare dans ce sens que : « Même si un ingénieur écrit un composant logiciel et le documente en anglais par exemple, un autre ingénieur, soit-il un Anglais, peut interpréter cette documentation dans le mauvais sens.

Appel est connu notamment pour avoir participé au projet CompCert de l’Institut français de recherche en informatique. Leurs travaux à l’époque ont consisté à créer un compilateur capable de traduire fidèlement un langage de programmation en instructions-machine pouvant s’exécuter sur une carte à puce. Selon Appel, la suite logique des travaux actuels est de connecter les composants que sont les compilateurs, les systèmes d’exploitation, les outils d'analyse de programmes, les architectures processeurs en s’assurant qu’aucun bogue n’arrive à se faufiler entre eux. C’est l’un des objectifs de DeepSpec qui va faciliter cette intégration en améliorant la façon dont les spécifications sont rédigées en utilisant la logique formelle d’après Appel. Un autre chercheur ayant participé au projet CompCert du nom de Beringer a déclaré que le projet de l’Institut français de recherche en informatique a démontré qu’il est possible de rédiger des spécifications logicielles robustes pour des logiciels complexes de l’industrie. Il ajoute que ce modèle a été suivi par d’autres équipes sur des projets isolés dans la conception de composants logiciels. Cependant, selon lui, la force de DeepSpec est de rassembler les efforts de chacun des participants autour d’une même problématique.

Le projet est mené avec la participation de plusieurs grands noms dont Stephanie Weirich et Steve Zdancewic, tous deux professeurs au département d’informatique du MIT, Adam Chlipala, professeur agrégé en informatique au MIT, et Zhong Shao, professeur d’informatique à l’université Yale. Le travail d’Appel tournera autour des outils permettant de raisonner sur les programmes informatiques, celui de Steve tournera autour des compilateurs. Adam quant à lui va travailler sur les puces informatiques et Zhong se chargera de mettre en place un système d’exploitation vérifié, quant à Stéphanie, son travail va tourner autour des langages de programmation qui peuvent être utilisés par les développeurs pour écrire leurs programmes. Un autre membre de l’équipe du nom de Benjamin Pierce travaillera lui sur les outils de test logiciels qui vont se baser sur les spécifications.

Source : princeton.edu

Et vous ?

Que pensez-vous de ce projet ? Est-il réaliste ?