LIA INFINIS: méthodes formelles pour la modélisation, la spécification, la vérification et le développement de logiciels

« Il y a un bug… ». Cette phrase anodine, entrée dans le langage courant, et souvent associée à des problèmes mineurs, peut également se référer à des dysfonctionnements informatiques ayant des conséquences potentiellement dramatiques comme l’illustrent les exemples suivants.

– Therac-25 (1985) : hautes radiations
Therac-25 est le nom d’une machine de radiothérapie. Entre 1985 et 1987, le Therac-25 fut impliqué dans au moins six accidents durant lesquels des patients reçurent des doses massives de radiation, parfois de l’ordre de plusieurs centaines de grays. La cause directe du dysfonctionnement était d’ordre informatique.

– MIM-104 Patriot (1991) : interception manquée de missile
Le 25 février 1991 un missile irakien frappait les casernes de Dhahran, en Arabie saoudite, tuant 28 soldats du centre de commandement du 14e détachement de l’armée des États-Unis.
Une recherche gouvernementale a indiqué que l’interception manquée de Dharan avait été provoquée par une erreur de logiciel dans son système de coordination.

– Explosion de la fusée Ariane 5 (1996)
Le vol 501 est le vol inaugural du lanceur européen Ariane 5, qui a eu lieu le 4 juin 1996. Il s’est soldé par un échec, causé par un dysfonctionnement informatique, qui vit la fusée se briser et exploser en vol seulement 36,7 secondes après le décollage.

L’informatique est omniprésente dans notre société, que ce soit dans le domaine médical, l’industrie aéronautique, automobile ou chimique, les télécommunications, l’électronique, les banques, etc. Plusieurs logiciels utilisés dans ces domaines sont critiques, c’est-à-dire que leur dysfonctionnement peut entraîner des conséquences graves, comme des décès, des dégâts matériels importants, des pertes financières faramineuses, ou des séquelles irréversibles pour l’environnement. La complexité croissante de ces systèmes critiques pose de nombreux problèmes techniques dans tous les cycles de développement des logiciels : de l’expressivité des langages de programmation, aux étapes de test et/ou de certification, en passant par la conception, la spécification, la vérification, la mise en œuvre, etc.

Ce constat est le point de départ de l’activité de recherche du LIA INFINIS, qui s’est concentrée sur le développement de nouvelles méthodes formelles pour définir des formalismes rigoureux limitant au maximum les incompréhensions entre développeurs et utilisateurs.

 

« Le LIA INFINIS a été créé en 2011 afin de renforcer la coopération scientifique entre la France et l’Argentine dans le domaine de l’informatique fondamentale. »

 

L’approche adoptée par INFINIS est basée sur des méthodes symboliques formelles, et en particulier, sur la construction de modèles permettant la définition de langages de programmation de haut niveau, la spécification aisée des propriétés de systèmes critiques, la possibilité d’automatiser la vérification de ces propriétés, et de les analyser de manière statique ou dynamique. Sachant que ces problèmes sont soit intrinsèquement indécidables ou souffrent de complexité théorique élevée, l’étude de la combinatoire, de la complexité algorithmique et de l’optimisation fait donc également partie du programme de recherche du LIA INFINIS.

Le LIA INFINIS a été créé en 2011 afin de renforcer la coopération scientifique entre la France et l’Argentine dans le domaine de l’informatique fondamentale. Il associe le CNRS, l’Université Paris Diderot, le Consejo Nacional de Investigaciones Científicas y Técnicas (CONICET) et l’Université de Buenos Aires. Le LIA INFINIS organise un workshop annuel, contribue à la formation des étudiants et de jeunes doctorants, et facilite les échanges de chercheurs entre les deux pays, y compris de longs séjours académiques.

 

→ Contacts:
Delia Kesner: kesner@irif.fr
Sergio Yovine: syovine@dc.uba.ar

Retour au sommaire