Manuscrit

Telecharger le manuscrit directement au format pdf : HDR Thomas Polacsek version simple (pdf)

Manuscrit disponible sur : HAL archives-ouvertes (version soutenue)

Manuscrit au format epub (pour liseuses) : HDR Thomas Polacsek version simple (epub)

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.