Les méthodes générales : assertions, réécriture, interprétation abstraite, logiques et assistants de preuve

En 1963, dans un article fondateur militant pour le traitement mathématique de la programmation et introduisant une brochette remarquable de nouveaux concepts, J. McCarthy a introduit l’idée bien différente d’utiliser la réécriture de termes comme outil applicable à la fois pour l’optimisation de programmes et leur vérification formelle. Cette approche, la seconde que nous étudierons, a eu une longue descendance dans les systèmes de vérification (Boyer&More, ACL2, PVS, Key, ProVerif, etc.), et continue d'irriguer les autres approches. Elle a eu des succès remarquables en circuits, en avionique, en sécurité, etc.

La troisième approche historique est celle de la sémantique dénotationnelle des langages introduite par Scott et Strachey vers 1970. Ici, un programme est interprété comme une fonction dans un espace topologique ordonné par un ordre d’information, et toutes les fonctions sont rendues totales par l’ajout explicite d’éléments indéfinis. Une théorie générale du point fixe dans les espaces ordonnés permet d’interpréter de façon uniforme les boucles, la récursion et la programmation fonctionnelle d’ordre supérieur. Au début des années 1970, cette théorie a été à l’origine du pionnier des assistants de preuve de programmes, LCF, créé par Milner et al. Mais le traitement explicite de l’indéfini s’est révélé trop compliqué, et les assistants de preuve ont ensuite suivi un autre chemin. La sémantique dénotationnelle a cependant eu un succès considérable dans une autre approche de la vérification, l’interprétation abstraite créé par P. et R. Cousot en 1977. L’idée est ici de travailler avec des assertions portant non plus sur les valeurs exactes calculées, mais sur une abstraction de celles-ci, comme la preuve par 9 le fait pour détecter des erreurs dans la multiplication. De nombreux domaines abstraits ont été développés, ainsi que des méthodes algorithmiques générales de combinaison de ces domaines et d’accélération des calculs de points fixes. L’interprétation abstraite est maintenant développée industriellement. Elle a permis de vérifier des propriétés critiques de très gros programmes, comme l’absence d’erreurs à l’exécution dans le code de pilotage de l’Airbus A380. Elle est également utilisée pour l’évaluation du temps de calcul maximal de logiciels embarqués et pour accélérer les calculs dans d’autres types de système de vérification.

La quatrième approche traitée dans ce cours est la vérification par assistants de preuves logiques. L’idée est ici de traduire le problème de vérification informatique en un problème purement logique, et de fournir une aide à la vérification à travers un système de tactiques et d’interaction homme-machine permettant d’organiser les preuves logiques à grand échelle, augmenté d’automatisations partielles pour des sous-domaines spécifiques utilisant par exemple des techniques de réécriture. Les assistants actuels traitent plusieurs types de logique, allant du calcul des prédicats de premier ordre augmenté par la théorie des ensembles (Rodin pour Event B, etc.) ou par la logique temporelle (TLA+), jusqu’aux calculs d’ordre supérieur (HOL, Isabelle, Coq, etc.). Ce cours présentera sommairement les ateliers de premier ordre, les ordres supérieurs étant traités dans le cours suivant. Nous prendrons l’exemple des formalismes B et Event-B de J.-R. Abrial (orateur du dernier séminaire du 1^er avril 2015). L’atelier B a été utilisé pour la spécification, la programmation et la vérification formelle de logiciels critiques pour la conduite du RER A, de la ligne 14 (Meteor) du métro parisien, et de plusieurs autres systèmes ferroviaires. Event-B et son système Rodin sont une évolution de B vers les systèmes événementiels qui sont ubiquitaires dans l’informatique embraquée.