Faites-vous confiance à votre thermostat ?

Pour obtenir des garanties fortes sur des programmes informatiques, dans le cas où ces programmes sont exécutés dans un contexte où aucune erreur n’est permise, plusieurs techniques peuvent être employées. En plus des méthodes industrielles visant à certifier l’ensemble du développement par rapport à certaines normes, les méthodes formelles proposent une approche basée sur des raisonnements mathématiques permettant de garantir formellement qu’un programme respecte certaines propriétés.

Une classe de programmes en particulier représente un enjeu important : les systèmes embarqués critiques. Ces systèmes, pour lesquels une anomalie pourrait mettre en danger des vies humaines, reposent sur un modèle d’exécution particulier : ils interagissent entre eux et avec le monde réel au cours du temps. Bien sûr, tous les systèmes embarqués ne sont pas systématiquement critiques : prenons l’exemple d’un thermostat, les garanties de sûreté requises sont plus fortes s’il est intégré au sein d’un système de refroidissement de centrale nucléaire qu’au sein de votre installation de chauffage domestique ! Les langages synchrones sont une classe de langages indiquée spécialement pour le développement de tels systèmes, et les principes sur lesquels ils reposent en font d’excellents candidats à l’application des méthodes formelles.

Dans le processus de développement de toute application, il existe une phase de traduction : la compilation. La compilation consiste à rendre compréhensible par l’ordinateur un programme écrit par un humain. Pour s’assurer que le code qui sera finalement exécuté est correct et sans bugs, il ne suffit donc pas d’avoir des garanties sur le programme source, il faut également avoir des garanties sur ce processus de compilation. Dans l’absolu, il faudrait en plus obtenir des garanties sur l’ordinateur lui-même, le matériel sur lequel s’exécute le code compilé. En laissant de côté cette dernière question, qui fait l’objet d’un champ de recherche à part entière, peut-on réussir à prouver que la compilation d’un programme écrit en langage synchrone est correcte ?

Quand la confiance devient un enjeu critique

Certains systèmes utilisent des composants logiciels dans lesquels la présence d’erreurs, de bugs, peut avoir des répercussions dramatiques. C’est par exemple le cas des systèmes de commandes de vol des avions, des systèmes de contrôle des centrales nucléaires ou des systèmes de commande des métros automatiques. On parle de systèmes critiques. Pour de telles applications, il est donc nécessaire d’avoir une confiance très élevée dans la sûreté et la correction du code informatique qu’elles utilisent.

Pour garantir de tels niveaux de confiance, l’état de l’art est de s’assurer que tout le processus de développement des composants logiciels critiques soit conforme à un ensemble de normes industrielles standardisées. Cela implique les méthodes de programmation, les choix de langages de programmation, ou encore les procédures de tests. En parallèle, un pan de la recherche en informatique s’intéresse à ce que l’on appelle les méthodes formelles. Cette approche regroupe un ensemble de techniques basées par exemple sur des calculs et de la déduction logique et permettant de raisonner formellement sur des programmes. Ces méthodes offrent l’avantage de pouvoir garantir dans le meilleur cas le niveau le plus élevé de confiance : une preuve mathématique que le logiciel respecte telle ou telle propriété.

Quelle que soit la méthode utilisée, les garanties de confiance sont généralement obtenues sur le programme source. Mais le programme, écrit dans un langage compréhensible par le programmeur, n’est pas intelligible tel quel par l’ordinateur. Il doit lui être traduit, dans ce que l’on appelle le langage machine. Ce travail difficile est confié à un autre programme, appelé compilateur (voir l’article Demandez le programme). Mais que faire si le compilateur lui-même est « buggé » ? Si l’on ne peut pas s’assurer que le compilateur fait bien son travail, alors les garanties obtenues sur le programme source sont caduques sur le programme qui finira réellement par être exécuté par l’ordinateur après sa compilation. Ce constat, qui fait du compilateur le maillon faible de la chaîne, est à l’origine de nombreuses avancées récentes qui couronnent plus de 50 ans de recherche : le développement de compilateurs vérifiés formellement. De tels compilateurs, comme le compilateur CompCert pour le langage C  (voir l’article Comment faire confiance à un compilateur ?), sont développés à l’aide d’assistants de preuve qui permettent d’établir une preuve mathématique de leur correction. Un compilateur est correct s’il préserve la sémantique, autrement dit, si le comportement du programme est le même avant et après sa compilation. CompCert est capable de compiler des programmes écrits en langage C, un langage qui, bien que très utilisé dans le monde des systèmes critiques, n’est pas nécessairement le plus indiqué pour leur développement.

Systèmes embarqués et langages synchrones

Les composants logiciels des systèmes critiques donnés en exemple précédemment appartiennent à une classe plus précise appelée systèmes embarqués temps réel, ou systèmes réactifs. Ce sont des logiciels intégrés au sein de systèmes plus larges (l’avion, la centrale, le métro…) qui interagissent avec le monde physique au cours du temps. Revenons à l’exemple plus simple et non critique du thermostat domestique : intégré au sein de votre système de chauffage, le logiciel de contrôle va obtenir une mesure de la température actuelle à l’aide de capteurs et ajuster la commande (plus chaud, moins chaud), tout cela en boucle.

Avec la fin des années quatre-vingts et l’essor des systèmes embarqués critiques, il devint apparent que les langages habituellement utilisés, comme le langage C, ou même l’Assembleur (l’Assembleur est le dernier langage compréhensible par des programmeurs avant le langage machine) étaient inadaptés à leur développement. En effet, ces langages dits impératifs ne proposent pas de fonctionnalités permettant de refléter simplement et de façon sûre le modèle particulier d’exécution des systèmes réactifs. Les langages dits synchrones (voir la section Les langages et les paradigmes de l’article Demandez le programme) pallient ce manque. Ils permettent de décrire l’interaction concurrente de plusieurs composants sur une échelle de temps discrétisée, c’est-à-dire que le temps est vu comme une succession de tics d’horloge (on parle aussi de cycles d’horloge). Chaque composant lit ses entrées et produit ses sorties dans le même tic, on peut donc le considérer comme une fonction produisant un flot infini de valeurs de sortie, synchrone avec son flot infini de valeurs d’entrée.

Ces langages permettent non seulement de décrire au mieux les systèmes réactifs comme les systèmes de contrôle / commande (le thermostat, les commandes de vol, etc.) mais aussi de fournir un modèle mathématique simple pour le raisonnement, faisant d’eux des candidats idéaux à l’application des méthodes formelles et répondant donc à l’enjeu critique. L’un de ces langages, Lustre, inventé en 1987 par une équipe de chercheurs français, permet de donner une traduction sous forme de programmes des schémas-blocs, représentation graphique bien connue des automaticiens et ingénieurs spécialisés dans les systèmes de contrôle / commande. Lustre est par exemple au cœur de l’outil d’ingénierie SCADE spécialisé dans le développement de systèmes critiques réactifs, et qui fournit un compilateur capable de traduire du code Lustre en code exécutable sur un ordinateur embarqué. Ce compilateur est certifié industriellement, et un grand niveau de confiance lui est accordé. Une question scientifique intéressante cependant : peut-on prouver mathématiquement parlant qu’un compilateur comme celui de SCADE est correct ?

Figure 1 : Détail d’un schéma-bloc d’un système de contrôle de fauteuil roulant électrique dans l’outil SCADE. Les blocs représentent des opérateurs et des sous-systèmes, dont les entrées et sorties sont reliées entre elles par des lignes, qui représentent des signaux, ou flots de valeurs. Ce schéma est en fait la représentation graphique d’un programme Lustre, amené à être compilé en un programme exécutable par l’ordinateur embarqué du fauteuil. Le schéma et le code Lustre sont considérés comme deux syntaxes alternatives pour le même programme : il n’y a pas ici à proprement parler de notion de traduction entre les deux. Source : Timothy Bourke

Prouver la compilation de Lustre

La compilation d’un programme Lustre vers du code impératif et exécutable est relativement simple. Chaque composant est traduit indépendamment vers une fonction dont l’exécution réalise un pas de calcul, durant un tic d’horloge. Le programme tourne en boucle : à chaque cycle, il lit ses entrées depuis l’extérieur, exécute le pas de calcul du composant principal, qui englobe tous les autres, et écrit ses sorties vers l’extérieur.

Figure 2 : Un schéma-bloc plus simple et le code Lustre correspondant. Le nœud, ou système, euler est une fonction prenant deux flots de valeurs flottantes x0 et u et renvoyant un flot x. Il implémente un schéma d’intégration dit d’Euler en avant avec un pas d’intégration constant de 0.1. Le nœud est défini par une équation qui spécifie les valeurs successives du flot x à l’aide d’opérateurs arithmétiques et de l’opérateur fby, qui implémente une mémoire (en automatique, on parle de délai unitaire).

Le défi, pour prouver qu’un compilateur Lustre est correct, est d’établir la préservation de la sémantique, comme discuté plus haut. Effectivement, les modèles d’exécution synchrone et impératif sont deux modèles très différents. En amont des fonctions de flots infinis, en aval des suites d’instructions qui modifient la mémoire de l’ordinateur. L’écart entre ces deux modèles rend la preuve du théorème de correction très difficile, mais pas son énoncé en lui-même, plutôt clair :

Si la compilation réussit, alors l’exécution du programme compilé produit en boucle les mêmes sorties que le programme source, à partir des mêmes entrées.

L’intérêt principal d’un tel théorème réside dans son exhaustivité : il est vrai quelles que soient les valeurs d’entrée et sortie considérées.

Figure 3 : Architecture de Vélus. Chaque bloc représente un langage intermédiaire, et chaque flèche une passe de traduction ou transformation de code. Les blocs en bleu sont des langages synchrones, en vert un langage de système de transitions, et en rouge des langages impératifs.

Le projet Vélus, développé au sein d’Inria par l’équipe de recherche PARKAS, est un compilateur académique qui traduit du code Lustre vers du code Assembleur. Il s’articule en une chaîne de passes de traduction vers plusieurs langages intermédiaires successifs, jusqu’au langage C, et intègre CompCert pour terminer cette chaîne jusqu’à l’Assembleur. Chacune de ces passes est prouvée correcte avec l’assistant de preuves Coq, et la composition de toutes les preuves permet d’établir la preuve du théorème de correction. Vélus permet donc d’affirmer que oui, il est possible de prouver que la compilation d’un programme écrit en langage synchrone est correcte, et ainsi d’obtenir un niveau de confiance très élevé dans le code généré.