Aujourd’hui, si la plupart des systèmes (automobile, train, avion, téléphone, magnétoscope…) combinent matériel et logiciel, leur sécurité passe souvent par la fiabilité de ce dernier. Or, d’une part, la correction d’un logiciel embarqué nécessite le rappel de tous les exemplaires du produit dans les services de maintenance, d’autre part, le temps de validation par les méthodes traditionnelles de test croît exponentiellement avec la complexité des systèmes.
• Pour améliorer la sécurité des systèmes, les méthodes formelles permettent leur validation automatisée à partir de leur modélisation. Elles ont pourtant encore des difficultés à être appliquées dans les industries, malgré de beaux succès comme la vérification automatique du système de freinage du métro Météor (ligne 14 à Paris), des systèmes de navigation des Airbus, de nombreux protocoles de transport de l’information dans les réseaux ou de plusieurs micro-processeurs.
• C’est pour discuter et améliorer ces méthodes que l’équipe Techniques formelles et à contraintes du LIFC — laboratoire d’Informatique de l’université de Franche-Comté — organise la 6e édition du congrès AFADL, groupe national soutenu par le CNRS au sein du groupe de recherche Algorithmique, langage et programmation.
Jacques Julliand – Bruno Tatibouet
LIFC
Université de Franche-Comté
Tél. 03 81 66 65 15
guillemot@lifc.univ-fcomte.fr
http://lifc.univ-fcomte.fr/afadl2004
