Accueil du site > Vie de la recherche > Actualités scientifiques




Recherchez sur ce site


Gérard Berry et la preuve par ordinateur

La notion de preuve informatique est aussi vieille que l’existence des programmes. En effet, il est nécessaire, dans de nombreux domaines, de certifier la fiabilité de ces derniers. Quels sont les principes permettant de valider le bon fonctionnement d’un programme, et sous quel aspect Gérard Berry s’est-il penché sur cette problématique ? Ce sont les questions auxquelles répond Christine Paulin-Mohring, professeur à l’Université Paris-Sud et membre de l’équipe de recherche VALS du Laboratoire de Recherche en Informatique (LRI, CNRS/Université Paris-Sud) et du projet TOCCATA commun avec Inria Saclay – Île-de-France.

Cet article est publié dans le cadre de notre série consacrée aux travaux de Gérard Berry, lauréat de la médaille d’or du CNRS en 2014-.

Comment avez-vous connu Gérard Berry et quelles ont été vos premières collaborations ?

Je connais Gérard Berry de réputation depuis que j’ai commencé mon travail de recherche. A l’époque, on le connaissait surtout pour ses travaux sur la séquentialité, le lambda calcul, que l’on étudiait en cours. Les premières interactions directes sur le plan scientifique se sont produites au début des années 1990, période à laquelle certains ponts ont été établis entre ses travaux sur Esterel et les langages synchrones d’une part, et les travaux sur les outils de preuve assistés par ordinateurs d’autre part.

Les langages synchrones comme Esterel sont utilisés dans des programmes critiques et mettent en œuvre des techniques complexes pour la vérification et la génération de code. Par exemple, dans le domaine de l’aviation, le processus de certification est obligatoire pour apporter des garanties sur l’absence d’erreurs dans le code critique. L’idée qui émergeait à l’époque était d’apporter la garantie la plus forte possible à savoir une preuve mathématique complètement formalisée dans un assistant de preuve (à savoir l’assistant Coq sur lequel mon équipe travaillait) de la correction du générateur de code Esterel. L’idée générale est qu’en utilisant de meilleurs langages sur lesquels il est possible de raisonner, on peut garantir certains comportements des programmes sans avoir à faire de tests a posteriori, ce qui est coûteux sans être complètement sûr.

Comment apporte-t-on la preuve de la fiabilité d’un programme ?

Il faut tout d’abord établir une description de ce que l’on attend du programme, ce qui peut sembler simple mais n’est pas toujours facile à faire. En effet, le comportement du programme dépend de ce qui se passe autour, ce qui nécessite de modéliser l’environnement avec lequel il interagit (capteurs, systèmes malveillants). Ensuite, il s’agit de traduire la méthode de vérification du programme en un problème mathématique.

Il faut savoir que le comportement des langages de programmation généralistes n’est pas toujours bien défini et qu’un même programme peut se comporter différemment suivant la machine utilisée. D’où l’intérêt des travaux comme ceux de Gérard Berry, avec Esterel, pour concevoir des langages propres, prédictibles. Une fois que l’on a une description de ce que va faire le programme et une description mathématique du comportement attendu, on peut construire la preuve mathématique qu’il y a bien adéquation entre les deux.

Dans certains cas, on peut établir la preuve que le programme est conforme à la spécification de manière complètement automatique par calcul. Mais il existe aussi des problèmes qui ne pourront jamais être résolus par des machines, donc l’humain doit intervenir pour apporter des éléments de preuve.

Quelles sont les perspectives dans ce domaine de recherche ?

Le domaine est très vaste ! Il y a plusieurs pistes. D’abord il faut que les différentes techniques de vérification de programmes (test, analyse statique, model-checking, preuve déductive) s’auto-enrichissent de façon à ce que les outils mis à disposition dans les équipes de développement soient polyvalents et plus facilement utilisables, de façon à ce que l’on puisse limiter le nombre de bugs. Il faut également garantir toute la chaîne de production : de la description de haut niveau jusqu’au code machine embarqué. On connait actuellement des méthodes qui permettent de produire des codes sans défauts mais qui sont très coûteuses et complexes à mettre en place. Une perspective est de développer un certain nombre de briques d’usage général comme des noyaux système, des compilateurs, des bibliothèques qui sont très largement utilisées et qui sont souvent d’une grande complexité. L’utilisation de ces composants sûrs permet de limiter les erreurs sans effort supplémentaire de l’utilisateur.

Il y a beaucoup de domaines d’application dans lesquels il faut faire entrer la culture des preuves informatiques. Par exemple, cette culture est bien ancrée dans le domaine de l’aéronautique, qui doit faire face à des exigences très fortes du point de vue de la sécurité et donc du bon fonctionnement des programmes et qui s’appuie depuis plusieurs années sur des outils et méthodes avancées. Mais dans les secteurs de l’automobile, ou de la santé par exemple, ce n’est pas encore le cas, ce qui peut causer de gros problèmes en termes de sécurité ou de confidentialité.

Retrouvez les autres articles de notre série :
- Programmer le matériel : contributions du langage Esterel de Gérard Berry (avec Jean Vuillemin)
- Gérard Berry et la preuve par ordinateur (avec Christine Paulin-Mohring)
- L’informatique au service de l’aéronautique : les contributions de Gérard Berry (avec Emmanuel Ledinot, et Gérard Ladier)
- L’ordinateur musicien : les apports du langage Esterel, conçu par Gérard Berry, à la musique mixte (avec Arshia Cont) (à venir)
- Gérard Berry et les neurosciences (avec Yves Frégnac et Sophie Denève)