Discussion :

[Victor Vincent]

DeepSpec : un projet logiciel qui permettra de développer des logiciels sans bogues ?
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 ?

[qvignaud]

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é…

[Invité]

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...

[jmv]

On est déjà le 1er avril ?

[NSKis]

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

[super_navide]

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 ....

[maske]

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 ?

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.

[abriotde]

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).

[Invité]

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é.

Et puis au pire, ils prouveront que c'est impossible.

C'est à dire ? Ne pas trouver de solution prouve l'absence de solution ?

[maske]

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.

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.

[DonQuiche]

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.

[Matthieu Vergne]

Pour moi, le projet est ambitieux car, s'il est vrai qu'en théorie on peut s'assurer de ne pas avoir de bogue, dans le sens comportement non prévu et non souhaité (en faisant du formel on peut tout prévoir, quitte à ce que ce soit statistique s'il y a de l'aléatoire), dans la pratique on se heurte à 2 difficultés majeures :
- la difficulté d'établir le cahier des charges "parfait" (qui spécifie effectivement le système dont on a besoin)
- la difficulté de formaliser le cahier des charges sous forme de règles d'inférence évaluables (il faut s'assurer d'avoir une description assez précise pour pouvoir la décrire de manière formelle, et aucune règle sujette au problème de l'arrêt)

Le second problème peut être réglé en suivant des procédures permettant de n'avoir que des règles évaluables, au prix d'un gros effort de réflexion et de compromis. C'est déjà utilisé pour les trains et les avions (système critiques oblige avec nombreuses vies à la clé), mais comme le mentionne DonQuiche seulement sur des parties bien précises, et il leur faut donc étendre cette application à l'ensemble de l'environnement. Le premier problème en revanche est de l'ordre du besoin humain, comme l'a mentionné super_navide, et ne peut donc pas se voire réglé de manière formelle car on joue là avec des non-dits. Autrement dit, on peut s'assurer de faire des programmes sans bogues (i.e. qui implémentent exactement le cahier des charges), mais pas s'assurer que ce système soit effectivement ce dont le client a besoin (i.e. que le cahier des charges correspond au besoin réel du client). Un effort conséquent, mais tout autre, reste donc à faire au niveau de l'établissement du cahier des charges, et là on sort des techniques formelles pour utiliser d'autres techniques de l'ingénierie des exigences.

@abriotde : je pense que tu parles du problème de l'arrêt, et s'il est vrai que ce n'est pas décidable, on parle là de manière générale : on ne peut pas établir un algorithme qui permette de fournir une réponse pour toutes les machines de Turing. En revanche on peut prendre des contraintes supplémentaires (i.e. ne s'occuper que d'une catégorie spécifique de machines de Turing) où le problème est décidable. Et c'est là mon second point en début de post, où le problème est de s'assurer que cette catégorie est assez large pour couvrir l'ensemble des besoins de manière satisfaisante.

[dlandelle]

Je me souviens avoir programmé en ADA, c'était déjà un progrès considérable comparé à C++. Le typage est extrêmement fort, et c'est pas facile d'arriver à compiler. Mais après ça roule. La gestion des exceptions est très bien faite, et un plantage est très vite identifié.

Je ne vois pas bien ce qu'on peut faire de plus, les bugs provenant très souvent d'erreur de conception plus que de la programmation !!!

Je pense que ce projet concerne les équipes de développements peuplées d'incompétents qui en sont encore à faire des erreur de programmation de débutant.

Le but est toujours le même : confier le peu de boulot qui reste à des copains sur des critères de sélection sociale (les potes francs-maçons pour faire court) et à des équipes de moins en moins qualifiées.

Dans tous les métiers, pas que l'informatique, on outille au maximum pour que le boulot soit fait par des neuneux payés au smic, c'est une question de gestion, et de concentration du pouvoir, de dévalorisation du travail.

En plus, Yale est le berceau du Skull & Bones, la pire secte maçonique des USA, cela peut dont aussi être un écran du fumée pour du financement occulte de la secte de Yale...

[pvincent]

l'Institut français de recherche en informatique

mieux connu en France comme étant l'INRIA.

Le baratin nécessaire pour décrocher un contrat et financer une recherche universitaire contient toujours une part d'exagération, donc cette annonce n'est pas très surprenante. Comme les meurs universitaires françaises se rapprochent peu à peu des meurs américaines, dans lesquelles décrocher des contrats de recherche est vital pour un laboratoire, j'espère voir bientôt des annonces similaires de la part d'équipes françaises, même si je doute que le fait d'avoir fait partie de l'INRIA soit un argument important dans notre pays pour obtenir 10 millions d'euros.