Lundi 9 septembre 2019 à 9h30 à l'IRIT

Soutenance habilitation à diriger des recherches (HDR) de Thomas Polacsek

Titre : Vérification, validation, certification : approches formelles et informelles pour établir la correction des artefacts et des logiciels

Lieu : auditorium J. Herbrand, au rez-de-chaussée de l'IRIT.

Si vous êtes aussi par là le mardi, n'hésitez pas à venir à la deuxième édition JET : Journée ingénierie des Exigences à Toulouse 2019

Comment venir

La soutenance aura lieu à l'auditorium J. Herbrand, au rez-de-chaussée de l'IRIT (Institut de Recherche en Informatique de Toulouse), Université Paul Sabatier 118 Route de Narbonne.

Itinéraire à partir de la gare ferroviaire Toulouse Matabiau
En métro : environ 30 minutes.
Prendre le métro ligne A direction "Basso-Cambo".
A la station "Jean-Jaurès", prendre le métro ligne B direction "Ramonville".
Descendre à la station "Université Paul Sabatier".

Itinéraire à partir de l’aéroport Toulouse Blagnac
En navette + métro : environ 50 minutes
Prendre la navette aéroport Tisséo
descendre à la station "Compans Caffarelli".
Prendre le métro ligne B direction "Ramonville".
Descendre à la station "Université Paul Sabatier".

Jury

Rapportrice Régine Laleau Professeure des universités Université Paris-Est Créteil
Rapporteur Daniel Le Berre Professeur des universités, Université d'Artois
Rapporteur Lionel Seinturier Professeur des universités, Université de Lille et directeur département informatique du CRIStAL
Marraine Florence Sèdes Professeure des universités, Université de Toulouse
Examinateur Philippe Besnard Directeur de Recherche CNRS, IRIT
Examinatrice Mireille Blay-Fornarino Professeure des universités, Université de Nice
Examinateur Óscar Pastor Professeur des universités et directeur du Centro de Investigación en Métodos de Producción de Software
Invité Claude Cuiller Ingénieur, Airbus

A propos

Les opérations de Vérification et de Validation sont assez intimement liées à l’informatique et à la simulation numérique. Réalisées au plus tôt, elles permettent de s’assurer qu’un objet, un artefact, est correctement construit et évitent de découvrir seulement au moment de l'utilisation que celui-ci ne correspond pas aux attentes voire est défectueux. Un exemple fréquemment donné concernant une erreur non détectée à la conception est celui de la sonde spatiale Mariner 1 détruite en vol suite à une défaillance des commandes de guidage.

Lors de cette soutenance nous évoquerons diverses méthodes permettant d’établir la correction des artefacts. Ces méthodes peuvent se classer en deux catégories avec, premièrement, ce qui relève de la preuve formelle et, deuxièmement, ce qui relève d’un processus argumentatif plus informel. Comme nous le verrons, les méthodes formelles consistent à construire des preuves mathématiques, et ce, généralement, au moyen d’un ordinateur. En ce sens, même si elle s’en est largement émancipée, la preuve formelle s’inscrit dans la lignée de l’intelligence artificielle. Pour leur part, les méthodes informelles relèvent plus d’une démarche discursive s’inscrivant dans le cadre de l’étude du bien-fondée d’une argumentation.

Manuscrit bientôt disponible...