[:fr]LIA INFINIS: méthodes formelles pour la modélisation, la spécification, la vérification et le développement de logiciels[:es]LIA INFINIS: métodos formales para la modelación, especificación, verificación y desarrollo de software[:]

[:fr]

« 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

[:es]

“Hay un bug…”. Esta frase que ha pasado a formar parte del lenguaje cotidiano y suele estar asociada a problemas menores, también puede hacer referencia a fallas informáticas graves, como se ilustra en los siguientes ejemplos:

-Therac-25 (1985): Altos niveles de radiación

Therac-25 es el nombre de una máquina de radioterapia. Entre 1985 y 1987, la Therac-25 sufrió al menos seis accidentes durante los cuales los pacientes recibieron dosis masivas de radiación, a veces de varios cientos de grises. La causa directa de la falla era informática.

-MIM-104 Patriot (1991): Interceptación fallida de misiles

El 25 de febrero de 1991, un misil iraquí impactó en el cuartel de Dhahran, Arabia Saudita, y mató a 28 soldados del centro de mando del 14º Destacamento del Ejército de los Estados Unidos. Una investigación del gobierno indicó que la fallida interceptación de Dhahran fue causada por un error de software en su sistema de coordinación.

-Explosión del cohete Ariane 5 (1996)

El vuelo 501 fue el vuelo inaugural del lanzador europeo Ariane 5, el 4 de junio de 1996. Terminó con una falla, causada por un mal funcionamiento de la computadora: el cohete se rompió y explotó en vuelo sólo 36,7 segundos después de haber despegado.

Hoy en día, la informática está en todos lados, ya sea en el campo de la medicina, la aeronáutica, la industria automovilística, la química, las telecomunicaciones, la electrónica o el sector bancario. Varios programas de software utilizados en estos campos son críticos, es decir, su mal funcionamiento puede acarrear graves consecuencias, como provocar muertes, grandes daños materiales, pérdidas financieras enormes o daños irreversibles en el medio ambiente. La creciente complejidad de estos sistemas críticos plantea muchos problemas técnicos en todos los ciclos de desarrollo de software: desde la expresividad de los lenguajes de programación, pasando por las etapas de diseño, especificación, verificación, aplicación, ensayo y/o certificación, etc., hasta el desarrollo de nuevo software.

Esta constatación es el punto de partida de la actividad de investigación del LIA INFINIS, que se ha centrado en el desarrollo de nuevos métodos para definir formalismos rigurosos que limiten al máximo los malentendidos entre desarrolladores y usuarios.

« Le LIA Infinis se creó en 2011 para reforzar la cooperación científica entre Francia y Argentina en el ámbito de la informática básica »

El enfoque adoptado por INFINIS se basa en métodos simbólicos formales y, en particular, en la construcción de modelos que permiten la definición de lenguajes de programación de alto nivel, la fácil especificación de las propiedades de los sistemas críticos, la posibilidad de automatizar la verificación de esas propiedades y de analizarlas de manera estática o dinámica. Sabiendo que estos problemas son intrínsecamente indecidibles o de una alta complejidad teórica, el estudio de la combinatoria, la complejidad algorítmica y la optimización es, por lo tanto, también parte del programa de investigación del LIA INFINIS.

El LIA INFINIS se creó en 2011 para reforzar la cooperación científica entre Francia y la Argentina en el ámbito de la informática básica. Asocia al CNRS, a la Universidad de París Diderot, al Consejo Nacional de Investigaciones Científicas y Técnicas (CONICET) y a la Universidad de Buenos Aires. El LIA INFINIS organiza un workshop anual, contribuye a la formación de estudiantes y jóvenes estudiantes de doctorado y facilita los intercambios de investigadores entre los dos países, incluyendo estancias académicas prolongadas.

→ Contactos:
Delia Kesner: kesner@irif.fr
Sergio Yovine: syovine@dc.uba.ar[:]

Partager cet article

Facebook
Twitter
LinkedIn

Articles similaires