Affichage des résultats du sondage: Que pensez-vous du projet DeepSpec ?

Votants
17. Vous ne pouvez pas participer à ce sondage.
  • Le projet n'est pas réaliste

    7 41,18%
  • Je suis optimiste

    0 0%
  • Le projet est ambitieux

    10 58,82%
  • Pas d'avis

    0 0%
+ Répondre à la discussion Actualité déjà publiée
  1. #1
    Chroniqueur Actualités

    Homme Profil pro
    Ingénieur développement logiciels
    Inscrit en
    janvier 2013
    Messages
    247
    Détails du profil
    Informations personnelles :
    Sexe : Homme
    Localisation : Sénégal

    Informations professionnelles :
    Activité : Ingénieur développement logiciels
    Secteur : High Tech - Éditeur de logiciels

    Informations forums :
    Inscription : janvier 2013
    Messages : 247
    Points : 6 450
    Points
    6 450
    Billets dans le blog
    1

    Par défaut DeepSpec : un projet logiciel qui permettra de développer des logiciels sans bogues ?

    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 ?

  2. #2
    Membre habitué
    Homme Profil pro
    Étudiant
    Inscrit en
    avril 2012
    Messages
    30
    Détails du profil
    Informations personnelles :
    Sexe : Homme
    Localisation : France, Loire Atlantique (Pays de la Loire)

    Informations professionnelles :
    Activité : Étudiant

    Informations forums :
    Inscription : avril 2012
    Messages : 30
    Points : 141
    Points
    141

    Par défaut

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

  3. #3
    Invité
    Invité(e)

    Par défaut

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

  4. #4
    jmv
    jmv est déconnecté
    Membre averti Avatar de jmv
    Profil pro
    Inscrit en
    mai 2004
    Messages
    369
    Détails du profil
    Informations personnelles :
    Localisation : France

    Informations forums :
    Inscription : mai 2004
    Messages : 369
    Points : 442
    Points
    442

    Par défaut

    On est déjà le 1er avril ?

  5. #5
    En attente de confirmation mail
    Femme Profil pro
    pape n'aimant pas les censeurs
    Inscrit en
    janvier 2010
    Messages
    803
    Détails du profil
    Informations personnelles :
    Sexe : Femme
    Localisation : Vatican

    Informations professionnelles :
    Activité : pape n'aimant pas les censeurs

    Informations forums :
    Inscription : janvier 2010
    Messages : 803
    Points : 1 358
    Points
    1 358

    Par défaut

    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

  6. #6
    Provisoirement toléré

    Profil pro
    Inscrit en
    juin 2003
    Messages
    382
    Détails du profil
    Informations personnelles :
    Âge : 42
    Localisation : France, Pyrénées Orientales (Languedoc Roussillon)

    Informations forums :
    Inscription : juin 2003
    Messages : 382
    Points : 0
    Points
    0
    Billets dans le blog
    1

    Par défaut Type de bug

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

  7. #7
    Membre éprouvé

    Homme Profil pro
    non
    Inscrit en
    mai 2008
    Messages
    395
    Détails du profil
    Informations personnelles :
    Sexe : Homme
    Localisation : France, Yvelines (Île de France)

    Informations professionnelles :
    Activité : non

    Informations forums :
    Inscription : mai 2008
    Messages : 395
    Points : 1 113
    Points
    1 113

    Par défaut

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

  8. #8
    Membre éprouvé
    Homme Profil pro
    Développeur informatique
    Inscrit en
    juillet 2007
    Messages
    553
    Détails du profil
    Informations personnelles :
    Sexe : Homme
    Âge : 35
    Localisation : France, Loire Atlantique (Pays de la Loire)

    Informations professionnelles :
    Activité : Développeur informatique
    Secteur : High Tech - Opérateur de télécommunications

    Informations forums :
    Inscription : juillet 2007
    Messages : 553
    Points : 940
    Points
    940

    Par défaut Logiciel sans bogue veux dire langage sécurisé

    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).
    Tout ce que j'écris est libre de droits (Licence CC0) et je vous incite à faire de même.

  9. #9
    Invité
    Invité(e)

    Par défaut

    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 ?

  10. #10
    Membre éprouvé

    Homme Profil pro
    non
    Inscrit en
    mai 2008
    Messages
    395
    Détails du profil
    Informations personnelles :
    Sexe : Homme
    Localisation : France, Yvelines (Île de France)

    Informations professionnelles :
    Activité : non

    Informations forums :
    Inscription : mai 2008
    Messages : 395
    Points : 1 113
    Points
    1 113

    Par défaut

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

  11. #11
    Expert confirmé Avatar de DonQuiche
    Inscrit en
    septembre 2010
    Messages
    2 744
    Détails du profil
    Informations forums :
    Inscription : septembre 2010
    Messages : 2 744
    Points : 5 442
    Points
    5 442

    Par défaut

    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.

  12. #12
    Expert confirmé
    Avatar de Matthieu Vergne
    Homme Profil pro
    Consultant IT, chercheur IA indépendant
    Inscrit en
    novembre 2011
    Messages
    1 882
    Détails du profil
    Informations personnelles :
    Sexe : Homme
    Localisation : France

    Informations professionnelles :
    Activité : Consultant IT, chercheur IA indépendant
    Secteur : High Tech - Éditeur de logiciels

    Informations forums :
    Inscription : novembre 2011
    Messages : 1 882
    Points : 5 973
    Points
    5 973
    Billets dans le blog
    2

    Par défaut

    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.
    Site perso
    Recommandations pour débattre sainement

    Références récurrentes :
    The Cambridge Handbook of Expertise and Expert Performance
    L’Art d’avoir toujours raison (ou ce qu'il faut éviter pour pas que je vous saute à la gorge {^_^})

  13. #13
    Nouveau membre du Club
    Homme Profil pro
    Directeur technique
    Inscrit en
    février 2010
    Messages
    49
    Détails du profil
    Informations personnelles :
    Sexe : Homme
    Localisation : France, Indre et Loire (Centre)

    Informations professionnelles :
    Activité : Directeur technique
    Secteur : High Tech - Multimédia et Internet

    Informations forums :
    Inscription : février 2010
    Messages : 49
    Points : 38
    Points
    38

    Par défaut ADA etc.

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

  14. #14
    Membre confirmé
    Profil pro
    Retraité
    Inscrit en
    novembre 2009
    Messages
    284
    Détails du profil
    Informations personnelles :
    Localisation : France

    Informations professionnelles :
    Activité : Retraité

    Informations forums :
    Inscription : novembre 2009
    Messages : 284
    Points : 523
    Points
    523

    Par défaut

    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.
    GraceGTK: a plotting tool at http://gracegtk.sourceforge.net

Discussions similaires

  1. Développement des logiciels en ligne
    Par Dev_info dans le forum Langages de programmation
    Réponses: 2
    Dernier message: 14/09/2012, 15h19
  2. Réponses: 4
    Dernier message: 11/04/2012, 15h44
  3. Réponses: 7
    Dernier message: 22/07/2008, 21h04

Partager

Partager
  • Envoyer la discussion sur Viadeo
  • Envoyer la discussion sur Twitter
  • Envoyer la discussion sur Google
  • Envoyer la discussion sur Facebook
  • Envoyer la discussion sur Digg
  • Envoyer la discussion sur Delicious
  • Envoyer la discussion sur MySpace
  • Envoyer la discussion sur Yahoo