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

Le présent manuscrit s’attache à donner une vue globale des travaux concernant les approches formelles et les approches informelles permettant d’établir la correction d’artefacts techniques, en général, et de logiciels, en particulier. L’établissement de cette correction s’inscrit dans ce que l’on nomme la vérification, la validation et la certification.Tous ces travaux se sont déroulés dans le cadre de projets et de partenariats industriels, comme les projets européens CRESCENDO et TOICA, des projets avec la Direction générale de l’Aviation civile (DGAC) et des partenariats avec la société Airbus. Si la majorité de ces travaux ont été réalisés dans le domaine aéronautique, et plus précisément dans les systèmes avioniques embarqués, ils ont aussi été appliqués au domaine médical.Une partie des résultats exposés ici s’inscrivent dans le cadre de deux thèses CIFRE réalisées par Anthony Fernandes Pires et Clément Duffau, thèses que j’ai co-encadrées. La première, réalisée en partenariat avec la société Atos, portait sur la vérification de programmes à l’aide d’une combinaison de méthodes formelles et d’Ingénierie dirigée par les Modèles. En ce qui concerne la deuxième, réalisée en partenariat avec la société Axonics, elle cherchait à définir un processus partant de l’élicitation d’exigences de justification pour aller jusqu’à leur production.Ces travaux ont été validés par des publications scientifiques, notamment dans les conférences CSCWD 2011 (best paper award) [150], CAISE 2013, 2015 et 2018 [53, 56, 65], MODELS 2013 [77], RCIS 2016 [148], ER 2017 [151], ICAPS 2018 [156] et dans le journal EURO Journal on Decision Processes [153].Concernant l’organisation de ce manuscrit, nous avons choisi une approche non chronologique avec un découpage suivant la dichotomie formelle / informelle. Dans le premier chapitre, nous montrerons que, dans un contexte historique de division du travail et de complexification des artefacts, la nécessité d’établir la correction de tout ce qui est produit s’impose d’elle-même. Par ailleurs, nous chercherons aussi à préciser notre vocabulaire et plus précisément les termes :artefact technique, vérification, validation, accréditation et certification. Le deuxième chapitre porte sur les approches formelles permettant d’établir la correction d’un artefact. Ainsi, nous verrons qu’il est possible d’utiliser des formalismes mathématiques et des ordinateurs afin d’établir automatiquement des preuves de correction. Cependant, tout ne pouvant se ramener à une forme formelle, nousverrons dans le troisième chapitre les avantages que nous pouvons tirer des travaux issus de l’argumentation pour organiser les justifications permettant d’établir la correction d’un artefact. Pour finir, le dernier chapitre est dévolu aux perspectives avec, d’une part, des perspectives s’inscrivant directement dans la continuité des travaux présentés dans ce manuscrit et, d’autre part, des perspectives concernant de nouveaux domaines de recherche pour lesquels j’ai déjà eu l’occasion de mener quelques travaux (concevoir des artefacts complexes fabricables, aider leschoix collaboratifs et les représentations cognitivement efficaces pour les modèles complexes)