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

Habilitation à diriger des recherches (HDR)

Soutenance le Lundi 9 septembre 2019 à l'IRIT, Toulouse

Manuscrit

Telecharger le manuscrit directement au format pdf : HDR Thomas Polacsek

Manuscrit disponible sur : HAL (archives-ouvertes)

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.

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