Ressource
Activité débranchée . Collège . Professeurs du secondaire . Jeu . Vidéo . vérification formelle de systèmes informatiques . Marie DuflotLa traversée de rivière.
Objectif : cette activité (débranchée) permet d’introduire la notion de vérification formelle de systèmes informatiques, et d’illustrer son utilité sur un exemple ludique.
Résumé : un pont en mauvais état, quatre personnes, quelques contraintes supplémentaires, et voilà le décor de l’activité posé. La question est alors de trouver le temps minimal de traversée pour ces personnes en respectant les contraintes. L’intérêt de cet exemple particulier est que l’intuition nous joue des tours, et que, sur ce problème assez simple (dans un vrai système informatique il y aurait bien plus de possibilités), on pense avoir la meilleure solution et on se trompe. On voit alors pourquoi un informaticien ne peut pas seul, en regardant simplement un programme, prétendre qu’il est correct.
Description du problème : quatre personnages veulent traverser un pont suspendu le plus rapidement possible. Seulement (sinon ce serait trop simple) le pont est en très mauvais état et il fait nuit, ce qui impose deux contraintes :
- le pont peut supporter maximum deux personnes à la fois (sinon il craque)
- il faut une lampe torche pour chaque traversée pour ne pas tomber, vu qu’il manque des planches sur le pont.
Malheureusement nos quatre personnes n’ont qu’une seule torche à se partager, et il faut donc qu’il y ait à chaque fois une personne (quelle qu’elle soit) qui ramène la torche. De plus, quand deux personnes traversent, le plus rapide doit attendre le plus lent sinon l’un des deux n’a plus de torche.
Les temps de traversée des personnages sont :
- 5 mn pour l’aventurière qui connaît le pont comme sa poche
- 10 mn pour Indiana Jones, en pleine forme mais qui découvre le pont
- 20 mn pour leur premier acolyte, blessé
- 25mn pour leur deuxième acolyte, plus gravement blessé.
Déroulé de l’activité : l’idée est de poser le problème et de laisser les enfants/élèves/personnes expérimenter. Il est très formateur de trouver une solution et d’essayer de l’améliorer, de rater, de se tromper dans son calcul de temps, de recommencer. La recherche de la solution optimale ne vient que dans un second temps. Si les participants ne trouvent pas la solution, on peut les guider vers ce qui fait perdre du temps (les deux personnages plus lents) et comment limiter cette perte de temps.
Lien avec l’informatique : se demander si son programme est correct, et s’il est le meilleur possible est une question que se posent les informaticiens. Cette activité montre qu’il n’est pas facile de trouver la solution « à la main ». Heureusement, certains informaticiens ont développé (et continuent à perfectionner) des méthodes ou des outils pour vérifier qu’un système informatique (un robot, un ordinateur, un avion, un aspirateur intelligent) fait bien ce qu’on attend de lui, et même pour évaluer ses performances. Dans le cas de la traversée de rivière, on parle de système « temporisé » car on a des indications précises sur le temps de chaque évènement, et on veut vérifier des propriétés qui nécessitent de chronométrer quelque chose. Il existe des logiciels qui peuvent vérifier automatiquement, et en une fraction de seconde, s’il est possible de faire traverser tous les personnages en strictement moins de 65 minutes. Ils peuvent même nous donner le temps minimum de traversée, et une stratégie pour y arriver. Les mêmes logiciels permettent sur des systèmes réels de dire s’ils font bien ce qu’on leur demande, et le cas échéant d’aider à les corriger.
Source : cette activité se base sur un exemple fourni avec le « model-checker » UppAal, un outil justement conçu pour, entre autres, vérifier des systèmes temporisés.
Age : cette activité fonctionne bien avec des collégiens, mais ce n’est pas le minimum !
Marie Duflot