DeepSpec : un projet logiciel qui permettra de développer des logiciels sans bogue ?
Une aventure du MIT et de quelques partenaires

Le , par Victor Vincent, Chroniqueur Actualités
Que pensez-vous du projet DeepSpec ?
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 ?


Vous avez aimé cette actualité ? Alors partagez-la avec vos amis en cliquant sur les boutons ci-dessous :


 Poster une réponse

Avatar de qvignaud qvignaud - Membre habitué https://www.developpez.com
le 09/01/2016 à 18:01
Citation Envoyé par Victor Vincent
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 solution à se qui peut être qualifiée comme une énigme à savoir la les comportements imprévisibles résultants de la mise ensemble de plusieurs programmes pour faire un travail donné.
Là ce n'est pas qu'un logiciel qui a bugué…
Avatar de - https://www.developpez.com
le 09/01/2016 à 18:08
Si je comprends bien, c'est un projet qui va changer l'industrie mais qui est réalisé uniquement par des universitaires.
C'est effectivement ambitieux...
Avatar de jmv jmv - Membre averti https://www.developpez.com
le 10/01/2016 à 2:45
On est déjà le 1er avril ?
Avatar de NSKis NSKis - En attente de confirmation mail https://www.developpez.com
le 10/01/2016 à 14:20
Après les "jeux à la protection incassable", voilà les "logiciels sans bugs"!

L'année 2016 commence fort... Et ce n'est pas fini Il va y avoir les "promesses électorales jamais tenues" des candidats à la présidentielle 2017!!!

Bonne nouvelle pour tous les barbus... Demain, on rase gratis
Avatar de super_navide super_navide - Provisoirement toléré https://www.developpez.com
le 10/01/2016 à 18:07
C'est totalement impossible de faire des programmes sans bug.

Il y a deux type de bug :
les bug techniques genre : accés a une position dans un tableau en dehors des limites , lecture d'un fichier qui n'existe pas etc...
les bugs fonctionnel : les bugs qui ne respectent pas les spécifications.

Pour la première catégorie c'est possible de faire des applications sans bugs.

Pour la seconde catégorie je pense que c'est impossible même en inventant un langage de spécification.
la raison est simple il y aura des erreurs dans la rédaction de la spécification et donc des bugs dans l'application car l'humain faire des erreurs ....
Avatar de maske maske - Membre éprouvé https://www.developpez.com
le 10/01/2016 à 20:34
Citation Envoyé par groharpon42 Voir le message
Si je comprends bien, c'est un projet qui va changer l'industrie mais qui est réalisé uniquement par des universitaires.
C'est effectivement ambitieux...
C'est à dire ?

Citation Envoyé par super_navide Voir le message
C'est totalement impossible de faire des programmes sans bug.
[...]
Pour la seconde catégorie je pense que c'est impossible même en inventant un langage de spécification.
la raison est simple il y aura des erreurs dans la rédaction de la spécification et donc des bugs dans l'application car l'humain faire des erreurs ....
Ils parlent de collecter des retours d'expériences et d'analyses de programmes pour changer la manière d'enseigner, pour justement améliorer la part strictement due «à l'humain».

Ensuite pour la partie «ambition», ça se base sur des travaux comme celui là https://hal.inria.fr/inria-00415861/document (lu y'a longtemps, me souviens pas des détails). Donc c'est pas forcément à balancer avant même que ça soit commencé. Et puis au pire, ils prouveront que c'est impossible.
Avatar de abriotde abriotde - Membre éprouvé https://www.developpez.com
le 10/01/2016 à 21:00
Il y a un théorème qui prouve qu il n est jamais possible de prouver l infaillibilité d un logiciel. Néanmoins il existe des moyen de sécurisé un logiciel et parfois d apporter certaines garantie. Java par la JVM garanti une sécurité (Valgrind pour C mais sur une exécution de simulation). Il existe aussi des vérificateur logique mais incappable de tout vérifier. Il y a aussi les simulation... Mais une des faiblesse fondamental sont les langages utilisés. Il me semble que Cobol bien que lourd et ancien apporte une certain sécurité tout en gardant la performance de C (contrairement a Java ou Python).
Avatar de - https://www.developpez.com
le 10/01/2016 à 21:35
Citation Envoyé par maske Voir le message
C'est à dire ?
Ils disent qu'ils veulent révolutionner l'industrie mais il n'y a aucun industriel dans leur projet. Ce sont peut-être des chercheurs géniaux mais il semblerait logique d'avoir aussi quelques personnes du milieu visé.

Citation Envoyé par maske Voir le message
Et puis au pire, ils prouveront que c'est impossible.
C'est à dire ? Ne pas trouver de solution prouve l'absence de solution ?
Avatar de maske maske - Membre éprouvé https://www.developpez.com
le 10/01/2016 à 22:03
Citation Envoyé par groharpon42 Voir le message
Ils disent qu'ils veulent révolutionner l'industrie mais il n'y a aucun industriel dans leur projet. Ce sont peut-être des chercheurs géniaux mais il semblerait logique d'avoir aussi quelques personnes du milieu visé.
Non c'est pas logique du tout. Il n'y a pas la prétention de prendre le boulot fait par les industriels et de le rendre «bug free». Ils veulent prouver que c'est possible et changer les méthodes et contenus d'enseignements en fonction - enfin ça reste de la spéculation parce qu'ils n'en sont qu'au stade projet mais je ne vois pas en quoi la présence d'industriels serait systématiquement obligatoire pour qu'un projet «à impact sur l'industrie» présente un intérêt et soit considéré comme sérieux.

Citation Envoyé par groharpon42 Voir le message
C'est à dire ? Ne pas trouver de solution prouve l'absence de solution ?
C'est pas comme ça que ça marche. Il n'y a pas d'histoire de «solution» à ce niveau. Si leur approche ne marche pas bien, leur boulot c'est de dire pourquoi et d'essayer de généraliser.
Avatar de DonQuiche DonQuiche - Expert confirmé https://www.developpez.com
le 11/01/2016 à 14:05
De quoi ça parle ? De méthodes formelles permettant de spécifier précisément, via la logique formelle, le comportement attendu d'un logiciel, puis de prouver que le code écrit est conforme à ces spécifications. Si besoin en assistant le logiciel dans la démarche de preuve.

Pour qui ? Des domaines critiques comme l'aéronautique, les centrales nucléaire, les microprocesseurs, etc.

Est-ce que c'est magique ? Non, prouver le fonctionnement d'un logiciel ou matériel est très coûteux. Mais nécessaire dans certains cas.

Est-ce que ça fonctionne ? Oui. Des systèmes de ce genre sont déjà utilisés dans l'industrie depuis longtemps pour le logiciel et le matériel.

Qu'est-ce qui est nouveau ? Celui-ci veut considérer simultanément tout l'écosystème logiciel (OS, pilotes, etc) pour vérifier leurs interactions. Les logiciels actuels considèrent chaque partie isolément.
Contacter le responsable de la rubrique Accueil