Du Lustre aux jolies leds

Au laboratoire Verimag, les scientifiques cherchent à aider les ingénieurs à prouver automatiquement que leurs programmes sont corrects.

Pour certains programmes, cette question est cruciale, car des vies sont en jeu, notamment quand il s’agit de systèmes embarqués (dans des avions, des trains, des voitures), mais elle est aussi difficile à cause de l'explosion combinatoire.

Une illustration de ce phénomène est donnée par l'échiquier de Sissa, sur lequel le nombre de grains de riz est doublé à chaque case: 1 grain sur la première case 1, 2 grains sur la suivante, puis 4, 8, 16, etc. Un tel échiquier comporte 2^64-1 grains de riz, c'est à dire plus de 18 milliards de milliards de grains, soit l'équivalent de 1000 ans de production mondiale de riz actuellement. Or un programme utilisant 64 cases (ou bits) est un petit programme, et vérifier qu'il est correct dans tous les cas de figure peut nécessiter de considérer des milliards de milliards de cas.

Au laboratoire Verimag, les axes de recherche visant à vérifier la correction de programmes critiques concernent la conception de langages de programmation, ainsi que des méthodes et des outils de preuve et de test automatisé.

Pour illustrer ces travaux, les chercheurs montreront comment vérifier la correction d'un petit programme embarqué sur une carte Arduino, comportant 2 entrées, actionnées par un bouton rouge et un bouton bleu, et 5 sorties, contrôlant l'allumage de 5 leds.

L'intégrité de ce système embarqué sera considérée comme compromise si une séquence d'entrée permet d'allumer les 5 leds simultanément. Le public pourra essayer de déterminer si différents programmes embarqués sur ce système sont dangereux (bogués), comme autant de petits puzzles.

>> Cet événement fait partie de Nuances de sciences 2019

>> Image : Pascal Wiemers, Flickr, licence cc