La recherche en méthodes formelles, pour les 30 années à venir

Résumé d'une présentation de Gilles Dowek, conférencier invité à NASA Formal Methods 2018

a marqué ce sujet comme résolu.
Auteur du sujet

Tout le monde se secoue ! :D

J’ai commencé (il y a 17 minutes) la rédaction d’un article au doux nom de « La recherche en méthodes formelles, pour les 30 années à venir » et j’ai pour objectif de proposer en validation un texte aux petits oignons. Je fais donc appel à votre bonté sans limites pour dénicher le moindre pépin, que ce soit à propos du fond ou de la forme. Vous pourrez consulter la bêta à votre guise à l’adresse suivante :

Merci !

Pour reprendre ce qui a été dit dans les commentaires tribune, ce qui est nécessaire pour l’instant (à mettre à jour selon ce que vous en direz) :

  • renommage de l’article
    • [On]
  • une petite note sur les pré-requis ? (savoir ce qu’est un programme et comment on le vérifie généralement ?)
    • [On] fin de l’intro, avant remerciements
  • ajouter un lien vers les slides de Gilles et vers le LSV
    • [On] fais dans l’intro
  • différences tests/preuves + complémentarité + quelques ressources
    • [On] Section 1, sous-section 1, après l’exemple
  • les guillemets autour de bon à supprimer ou préciser
    • [On] précisé dans la partie méthodes formelles
  • précision science informatique
    • [On] revu dans la "bio" de Gilles, traduction un peu malheureuse
  • exemple de livre pour les ouvrages de Gilles
    • [On] ajouté dans sa "bio"
  • Autres grands acteurs/méthodes utilisées spécifiques ?
    • [Off] ajout d’exemples d’acteurs dans l’intro sur les méthodes formelles,
    • [Off] ajout d’un bout sur Infer et Facebook aussi,
    • [Off] ajout d’un petit paragraphe dans la partie sur la NASA
  • précision sur la question comprendre VS prévoir
    • [On] modifié en reformulant l’exemple de la décimale de pi
  • citer le bouquin de Dan Ariely
    • [Off] Ajouté en secret
  • parenthèses sourcées pour la reconnaissance de style d’art
    • [On] fait, avec des articles non vulgarisés cela dit
  • revoir le début de la partie sur les concepts généraux en info
    • [On] reformulé
  • améliorer conclusion pour le fait que l’on ne répond pas à la question
    • [On] ajout d’un petit paragraphe dans la conclusion
  • exemple de défis actuels en méthodes formelles
    • parler du process de FB (voir plus haut)
    • voir pour des exemples plus généraux : usages commun en automobile, pénétration dans l’IoT, …
    • voir les liens de @Aabu.

Édité par Ksass`Peuk

First : Always RTFM - "Tout devrait être rendu aussi simple que possible, mais pas plus." A.Einstein [Tutoriel Frama-C WP]

+1 -0

Cette réponse a aidé l’auteur du sujet

Cool ! Quelques remarques (je me permets de commenter la forme tout de suite vu que le fond est solide) :

Introduction

la présentation de Gilles Dowek

Aurais-tu un lien (vers la présentation et vers plus d’infos sur ce chercheur, sa page perso par exemple) ?

Laboratoire Spécification et Vérification de l’ENS Cachan

Tu peux ajouter ce lien : http://www.lsv.fr/?l=fr

"que va-t-il se passer pour les méthodes formelles dans les 30 années à venir ?"

Tu pourrais utiliser un bloc "question".

Dans ce billet, je vous propose

C’est un article maintenant. ^^

Une petite note sur les pré-requis ?

Un peu de contexte

Par l’utilisation de tests, nous ne pouvons généralement pas montrer qu’un programme ne peut avoir que de "bons" comportements, dans la très vaste majorité des cas

Tu pourrais commencer une nouvelle phrase à partir de "dans la très vaste majorité des cas".

Par ailleurs, pourquoi mettre "bons" entre guillemets ? Je propose soit d’utiliser une formulation plus précise, sans guillemets, soit d’expliciter avec une note en quoi c’est une approximation.

et pas toutes les entrées possible

possibles

L’utilisation de ce type de méthode est revanche

en revanche

une autre paire de manches que sur terre

"Terre" ?

Par la suite, les projets ont connus

connu

les méthodes formelles sont l’un des nombreux domaines de recherche de la NASA

J’ignore si c’est à insérer ici, mais tu pourrais mentionner d’autres grands acteurs (entreprises, laboratoires) dans le domaine.

En outre, je me demande si les méthodes utilisées dépendent du domaine d’application ou non. La recherche menée à la NASA est-elle universelle ou spécifique à l’aérospatial (voire à leurs propres outils) ?

(théorie des types, théorie des ensembles, etc)

(vérification de preuve, preuve automatique de théorèmes, etc)

"etc." (avec un point).

des notions basiques de science informatique

Qu’entends-tu par "science informatique" ? Informatique en général (programmation par exemple) ou application des mathématiques à l’informatique ?

le ministère de l’éducation

"Éducation"

plusieurs livres scientifiques populaires

Des exemples des plus populaires ?

Merci pour le contenu et désolé pour le pinaillage.

+2 -0
Auteur du sujet

Merci pour tes retours. Ce que je n’ai pas encore réparé est ajouté dans le post de bêta en haut. Je me demande d’ailleurs comment vraiment fixer les pré-requis là dessus.

First : Always RTFM - "Tout devrait être rendu aussi simple que possible, mais pas plus." A.Einstein [Tutoriel Frama-C WP]

+0 -0

Cette réponse a aidé l’auteur du sujet

Mes retours sur la suite ci-dessous. Comme tu semblais vouloir modifier le fond, je ne me suis pas occupé de la forme. Une passe sur le style me parait assez judicieuse pour plus tard, en particulier pour supprimer quelques répétitions.

A propos des méthodes formelles, pour les 30 prochaines années

Ce n’est cependant pas une retranscription directe de la conférence, il contient

il ?

D’un côté nous voulons être surs que l’ordinateur nous transmet bien le bon résultat, mais en même temps nous ne voulons pas être capables de prévoir le résultat parce que sinon nous n’aurions pas besoin de l’ordinateur.

Tu pourrais rendre ce passage plus clair avec l’exemple de pi (ou un autre, ce qui permettrait de diversifier les exemples d’application) : nous voulons vérifier que le résultat obtenu est le bon mais ne voulons pas le faire en le comparant à une autre valeur que nous aurions obtenue par un autre moyen.

Attends-toi aussi à une question du lecteur au sujet des tests et en quoi ils diffèrent des méthodes formelles, dans quelle mesure ils sont complémentaires.

Dans le même temps, une libération de prison prononcée par un juge humain avant le repas a moins de 20% de chances d’être acceptée contre plus de 60% juste après le repas3, ce qui est tout sauf impartial, donc un algorithme n’aura pas un mal fou à se montrer plus impartial que cela.

Dan Ariely a écrit un bon bouquin sur les biais comportementaux : "Predictably Irrational".

la différence de style entre deux artistes s’ils appartiennent à des courants bien distincts (et ce serait aussi le cas pour des machines aujourd’hui).

Tu pourrais sourcer la parenthèse.

Quatre concepts en science informatique

Je n’ai pas compris le propos de cette partie.

Conclusion

Les méthodes formelles sont de plus en plus utilisées et s’attaquent aujourd’hui à de nouveaux défis.

Aurais-tu des exemples/sources ?


Je me demande d’ailleurs comment vraiment fixer les pré-requis là dessus.

Je dirais une culture générale basique en informatique, même si c’est imprécis. A minima, être familier avec la notion de programme informatique.

Je n’ai pas l’impression que l’article réponde concrètement à la question posée : "que va-t-il se passer pour les méthodes formelles dans les 30 années à venir ?". Tu mentionnes les enjeux généraux mais pas les pistes explorées pour y répondre. Quelle charge de travaille cela représentrait-il de recenser les grands axes de recherche actuels et probablement à venir ?

Merci !

+1 -0
Auteur du sujet

Bonjour les agrumes !

La bêta a été mise à jour et décante sa pulpe à l’adresse suivante :

Merci d’avance pour vos commentaires.

Attends-toi aussi à une question du lecteur au sujet des tests et en quoi ils diffèrent des méthodes formelles, dans quelle mesure ils sont complémentaires.

Je pourrais mettre ça dans l’intro, mais ça risque de grossir vite.

Dan Ariely a écrit un bon bouquin sur les biais comportementaux : "Predictably Irrational".

J’hésite à le citer, même si c’est effectivement intéressant. Je pense qu’il y a même pas mal de bouquins du genre. Mais je suis moyennement capable de juger la source. A la limite je peux le mettre en complément.

Tu pourrais sourcer la parenthèse.

Done, mais c’est pas du vulgarisé du coup.

Je n’ai pas compris le propos de cette partie.

J’ai détaillé, je pense que c’est mieux.

Aurais-tu des exemples/sources ?

Des sources et exemples, oui. Mais ça risque de finir au auto-pub, et en citation de papiers très techniques. C’est assez peu vulgarisé de ce côté.

(1) Je n’ai pas l’impression que l’article réponde concrètement à la question posée : "que va-t-il se passer pour les méthodes formelles dans les 30 années à venir ?". Tu mentionnes les enjeux généraux mais pas les pistes explorées pour y répondre. (2) Quelle charge de travaille cela représentrait-il de recenser les grands axes de recherche actuels et probablement à venir ?

(1) Il est vrai que cela ne donne qu’une piste. Je peux broder un peu plus la conclusion éventuellement pour dire que les recherches actuelles vont continuer et que d’autres sont naissantes. Mais, c’est comme le reste, c’est qu’une prédiction, et il est peu probable que ça se passe comme prévu.

(2) Probablement beaucoup. Il faudrait que je fasse une passe sur les grosses conférences du domaine sur au minimum les trois dernières années pour regarder les papiers de positionnement, les éditos et les types de projets financés en ce moment.

Merci pour tes retours.

Édité par Ksass`Peuk

First : Always RTFM - "Tout devrait être rendu aussi simple que possible, mais pas plus." A.Einstein [Tutoriel Frama-C WP]

+0 -0

Je pourrais mettre ça dans l’intro, mais ça risque de grossir vite.

Une phrase ou deux devraient suffire à apaiser le lecteur curieux. Pour celui encore plus curieux, tu pourrais fournir une ressource à ce propos. Sachant que s’il se pose la question, il a probablement un certain background donc elle n’a pas à être très vulgarisée.

Des sources et exemples, oui. Mais ça risque de finir au auto-pub, et en citation de papiers très techniques. C’est assez peu vulgarisé de ce côté.

Tu n’aurais pas des exemples simples du genre "En 2003, telle ville a vérifié son système de métros avec des méthodes formelles", "Facebook annonce une vérification formelle de telle partie de son système"… ? Ca fait écho à ma remarque sur les exemples d’application en fait.

Il est vrai que cela ne donne qu’une piste. Je peux broder un peu plus la conclusion éventuellement pour dire que les recherches actuelles vont continuer et que d’autres sont naissantes. Mais, c’est comme le reste, c’est qu’une prédiction, et il est peu probable que ça se passe comme prévu.

Peut-être alors renommer le contenu en "Les enjeux de la recherche formelle […]" ?

J’ai détaillé, je pense que c’est mieux.

En fait, c’est la première phrase ("Ces quatre concepts sont fixés empiriquement par le fait que chacun arrive à tomber dans un cas qui lui convient.") qui m’a perturbé, parce qu’elle fait suite au titre. Peut-être pourrais-tu la reformuler en quelque chose comme "La science informatique peut se diviser en quatre concepts, fixés empiriquement par le fait que chacun arrive à tomber dans un cas qui lui convient.".

Merci pour ton travail.

+0 -0
Auteur du sujet

Une phrase ou deux devraient suffire à apaiser le lecteur curieux. Pour celui encore plus curieux, tu pourrais fournir une ressource à ce propos. Sachant que s’il se pose la question, il a probablement un certain background donc elle n’a pas à être très vulgarisée.

J’ai passé ça dans la TODO list.

Tu n’aurais pas des exemples simples du genre "En 2003, telle ville a vérifié son système de métros avec des méthodes formelles", "Facebook annonce une vérification formelle de telle partie de son système"… ? Ca fait écho à ma remarque sur les exemples d’application en fait.

Pour le premier, ce n’est justement pas vraiment un nouveau challenge, le ferroviaire et consorts utilisent des FM depuis pas mal de temps. Facebook, oui ça pourrait le faire.

Peut-être alors renommer le contenu en "Les enjeux de la recherche formelle […]" ?

Je vais y réfléchir.

En fait, c’est la première phrase ("Ces quatre concepts sont fixés empiriquement par le fait que chacun arrive à tomber dans un cas qui lui convient.") qui m’a perturbé, parce qu’elle fait suite au titre. Peut-être pourrais-tu la reformuler en quelque chose comme "La science informatique peut se diviser en quatre concepts, fixés empiriquement par le fait que chacun arrive à tomber dans un cas qui lui convient.".

Han diantre. Bon c’est pas grave la fin est plus claire quand même je pense. J’ajoute ça dans la TODO list.

First : Always RTFM - "Tout devrait être rendu aussi simple que possible, mais pas plus." A.Einstein [Tutoriel Frama-C WP]

+0 -0

Tu n’aurais pas des exemples simples du genre "En 2003, telle ville a vérifié son système de métros avec des méthodes formelles", "Facebook annonce une vérification formelle de telle partie de son système"… ? Ca fait écho à ma remarque sur les exemples d’application en fait.

Pour le premier, ce n’est justement pas vraiment un nouveau challenge, le ferroviaire et consorts utilisent des FM depuis pas mal de temps. Facebook, oui ça pourrait le faire.

Ksass`Peuk

Les méthodes formelles commencent aussi à rentrer bien sérieusement dans l’automobile, où ils renforcent la sûreté et diminuent les risques de non-qualité.

Sur les équipements critiques (direction, système de freinage, régulation de vitesse, …) , il y avait déjà pas mal de redondance et de vérifications, y compris via des méthodes formelles. Ces méthodes se diffusent aux projets moins critiques (Polyspace passe sur tous les logiciels embarqués là où je travaille). Ces vérifications formelles sont intégrées dans le processus de qualité logicielle, en plus des tests.

Même sur des produits avec des enjeux de sûreté moins importants, les méthodes formelles renforcent la confiance dans le logiciel, en recherchant toute une gamme d’erreurs dures à détecter lors des tests (dépassements de capacité notamment). Quand le logiciel pilote un actionneur qui finit dans des centaines de milliers de voiture, tu diminues fortement le risque de rappels ou de mises à jour lors de la prochaine maintenance (ça coûte cher tout ça), et ça te permet de dégager des ressources pour les autres potentiels problèmes (mécaniques, thermiques, électronique, …), dont tu ne peux pas te débarrasser formellement.

+0 -0
Auteur du sujet

Mon problème n’est pas de savoir si ça existe, pour le coup je suis en plein dedans, mon problème est plus de trouver des sources qui ne soient pas direct des papiers de recherche (j’en ai déjà de trop en référence je trouve).

L’exemple de Facebook marche bien parce qu’il y a des articles plus généraux sur Infer. Mais sur le reste c’est moins facile. A la limite, il y a l’annonce Thalès/CEA pour les protocoles cryptos, il y a le modèle formel de ARM même si c’est plus si nouveau, le truc est complet.

First : Always RTFM - "Tout devrait être rendu aussi simple que possible, mais pas plus." A.Einstein [Tutoriel Frama-C WP]

+0 -0

Cette réponse a aidé l’auteur du sujet

Je ne sais pas ce que tu cherches comme source.

En dehors de la recherche, t’as les livres blancs des éditeurs de logiciel, qui sont destinés aux décideurs non spécialistes et montrent des gains concrets pour vendre leurs produits (tant de défaut en moins, tant de raccourcissement du temps de développement, …).

Il y a aussi des article dans la presse orientée industrie, qui montrent que c’est un créneau qui sort des labos.

+1 -0

Mon problème n’est pas de savoir si ça existe, pour le coup je suis en plein dedans, mon problème est plus de trouver des sources qui ne soient pas direct des papiers de recherche (j’en ai déjà de trop en référence je trouve).

Ca ne me semble pas problématique. Les exemples sont là pour donner une idée. Le lecteur souhaitant aller plus loin sur chacun peut probablement se confronter à un papier.

+0 -0
Vous devez être connecté pour pouvoir poster un message.
Connexion

Pas encore inscrit ?

Créez un compte en une minute pour profiter pleinement de toutes les fonctionnalités de Zeste de Savoir. Ici, tout est gratuit et sans publicité.
Créer un compte