Du Lustre aux jolies leds

Conception sûre de systèmes réactifs/embarqués/critiques, conception de langages, preuve automatique de programmes... autant de thèmes abordés lors de cette expérimentation d'allumage de leds

Village des sciences
  • Maths, physique, chimie
  • ,
  • Nouvelles technologies, numérique, informatique
  • Scolaires
  • Oui

Au laboratoire Verimag, nous cherchons à aider les ingénieurs informaticiens à prouver automatiquement que leurs programmes sont corrects.

  • La correction des programmes est cruciale, en particulier pour les systèmes embarqués, car des vies sont souvent en jeu.
  • Mais elle est difficile à cause de l'explosion combinatoire. Une bonne illustration de ce phénomène est donnée par l’échiquier de Sissa, comportant 1 grain de riz sur case 1, 2 grains sur la case 2, 4 sur la case 3, 8 sur la case 4, etc. Un tel échiquier comporte $2^{64}-1$ grains de riz, c'est à dire plus de 18 milliards de grains, soit l'équivalent de 1000 ans de production mondiale de riz actuellement. Or un programme de 64 cases (ou bits) est petit.

Plusieurs approches sont possibles pour faire face à cette difficulté. Au laboratoire Verimag, les axes de recherche visant à résoudre ce type de problèmes concernent :

  • la conception de Langages de programmation empêchant les programmeurs de faire certaines erreurs;
  • l'Analyse de programmes : conception d'algorithmes (des programmes aussi) qui essaient de prouver qu'un autre programme est « correct ».
  • l'automatisation des tests : conception d'algorithmes qui essaient de prouver qu'un programme n'est pas correct.

Pour illustrer ces axes de recherche, nous proposons une petite démonstration permettant de montrer

  • quelques exemples de programmes écrit en Lustre, un langage inventé au laboratoire et conçu pour mettre en œuvre des systèmes embarqués critiques ;
  • comment un tel programme peut-être embarqué sur un système (ici, une carte Arduino) ;
  • comment prouver automatiquement des propriétés sur ces programmes ;
  • comment tester automatiquement ces programmes.

Il s'agit donc de valider un petit système, composé d'un programme Lustre et d'une carte Arduino, comportant 2 entrées, contrôlées par un bouton rouge et un bouton bleu, et 5 sorties,représentées par 5 leds.

Nous proposons plusieurs programmes. Pour chacun d'eux, l'effet sur les leds d'une pression sur le bouton bleu ou le bouton rouge est différent. Mais à chaque fois, la propriété de sûreté que l'on veut vérifier est « il est impossible d'allumer les 5 leds ». Le public pourra essayer de résoudre ces petits puzzles, en essayant de déterminer s'il existe une séquence qui amène le système dans l'état dangereux. Nous montrerons ensuite comment des outils peuvent automatiser la réponse à ces petits puzzles.

Animateurs/conférenciers
Anne Rasse, Erwan Jahier, Benjamin Wack
Organisateur
Erwan Jahier
preuve de programmes, programmes réactifs, explosion combinatoire, test automatisé, langage de programmation, systèmes embarqués, arduino, 28 nuances de sciences

A propos du lieu

Bâtiment IMAG, 700 avenue Centrale, 38400 Saint Martin d'Hères
  • village des sciences

Grâce à plus de nombreux ateliers, les chercheurs manipulent sous vos yeux et vous font expérimenter les phénomènes scientifiques qu’ils côtoient chaque jour dans leurs labos

Accès: réservations pour les groupes : helene.deschamps@univ-grenoble-alpes.fr

28 Nuances de sciences : le village du Campus ! Communauté Université Grenoble Alpes

Créé par Erwan Jahier jeudi 24 août - 13:34

- Contacter