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

Tout le monde se secoue ! 

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.

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.

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.

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.

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.

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.

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.

Super merci, je regarderai ça.

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.

Bonjour les agrumes !

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

Merci d’avance pour vos commentaires.