41 milliards d’appareils connectés en 2025. L’Internet des Objets explose. Et avec lui, la complexité de conception de ces réseaux. D’autant plus qu’un simple changement sur une seule machine localement peut engendrer le dysfonctionnement de toute une architecture. Un des problèmes provient du fait que les développeurs peinent à préserver les propriétés de temps contrairement à celles liées à la mémoire. Au Centre Inria de l’Université de Rennes, le chercheur Benjamin Lion vient de recevoir une bourse post-doctorale Marie Skłodowska-Curie pour à la fois tenter d’intégrer ce facteur temps dans la sémantique des programmes et aussi de prouver formellement sa préservation durant la compilation. Cette recherche pourrait impacter le secteur industriel mais aussi permettre aux compilateurs de franchir un grand pas. Explications.
“À l’heure actuelle, le temps d’exécution est abstrait et, dans la plupart des cas, pas encore bien intégré dans la sémantique des langages. On doit garder à l’esprit que ce temps ne fait pas partie de la logique en soit. Il constitue un simple effet de bord, rappelle Benjamin Lion. Pourtant, il est très important, évidemment. Dans une usine, imaginez un bras manipulateur qui travaille sur une pièce. Le sens du programme se rapporte à l’impact physique que ce bras va exercer sur la pièce. La machine doit non seulement prendre en compte la logique des opérations, mais aussi les effets de bord comme le temps. Le programmeur doit donc maîtriser parfaitement le temps pour vérifier que la pièce est manipulée correctement.”
Idem pour l’Internet-des-Objets et les systèmes embarqués. “Si le temps entre deux instructions n’est pas bien compris, un robot, par exemple, peut s’être déplacé avant de recevoir la deuxième instruction. Auquel cas, celle-ci n’a peut-être plus de sens.”
Donner aux développeurs plus de prise
D’où le besoin de donner aux développeurs et à leurs programmes plus de prise sur la préservation des propriétés temporelles. Et c’est justement ce à quoi le post-doctorat de Benjamin Lion va s’atteler. Avec deux défis à relever.
Le premier vise à élaborer un cadre de développement présentant suffisamment d’expressivité pour spécifier les effets de temps sur les programmes. Mais aussi fournir des outils pour analyser les propriétés de chaque machine individuellement et les propriétés globales qui en résultent pour l’ensemble du réseau. “Dans l’idéal, la conception d’une application devrait s’approcher le plus possible de la manière dont raisonne le développeur pour que peu d’erreurs soient commises durant la spécification.”
Le but ici est de “développer une sémantique formelle qui intègre ces effets de temps et les propage par composition. Si vous exécutez un programme à la suite d’un deuxième, vous voulez raisonner sur le temps de tout le bloc en fonction du temps des deux parties. Et pour l’instant, on n’y parvient guère parce que l’on ne comprend pas vraiment comment le temps est composé. On se voit contraint de raisonner sur le bloc en entier.”
Benjamin Lion prévoit de se baser “sur une théorie mathématique existante. En utilisant une sémantique fonctionnelle avec des effets, on arrive à modéliser des effets dans une structure mathématique. Je souhaite instancier cette théorie mathématique pour propager le temps au cours de l’exécution. À ma connaissance, cela a été fait surtout pour raisonner sur des propriétés de mémoire, pas sur des propriétés de temps, bien que la théorie existe. Très probablement, vais-je devoir l’amender à certains endroits.”
Ces recherches sur le premier objectif se dérouleront en collaboration avec David Nowak, chercheur au CNRS. Autres scientifiques impliqués : Farhad Arbab (CWI Amsterdam) et Hans-Dieter Hiep (Université de Leiden et CWI Amsterdam), ainsi que Carolyn Talcott (Standford Research Institute). Le deuxième défi concerne le compilateur. Autrement dit, l’outil chargé de traduire le programme d’origine pour en faire du code binaire que le processeur se chargera ensuite d’exécuter.
Compilateur CompCert.
Et c’est là que CompCert entre en jeu. Conçu par Inria*, ce compilateur pour logiciels critiques a été prouvé formellement. Il offre une garantie mathématique qu’il génère du code binaire se comportant exactement comme le prescrit la sémantique du code source écrit en langage C. Cet outil a été prouvé correct à l’aide de Coq, un assistant de preuve lui aussi né de recherches à Inria.
“CompCert comporte un théorème de préservation de sémantique. Cette sémantique exprime non seulement la logique mais aussi les effets de mémoire, qui sont des efforts de bord. Et mon intention est d’étendre ce théorème pour qu’il puisse aussi exprimer et préserver les propriétés de temps. C’est un gros défi, mais si j’y parviens, un développeur pourra alors compiler un programme sensible au temps et préserver les propriétés temporelles durant l’exécution.”
Cette deuxième partie des recherches sera menée avec les membres d’Épicure, une équipe Inria* spécialisée dans les méthodes formelles dans laquelle travaille Frédéric Besson, qui a collaboré avec Benjamin Lion sur de précédents travaux.
Protocole UART
Si les choses se déroulent comme prévu, Benjamin Lion entreprendra ensuite de générer une implémentation certifiée pour UART. “Ce protocole permet la communication entre deux machines qui ne partagent pas la même fréquence d’horloge. L’industrie l’utilise beaucoup. Sur une chaîne d’assemblage, par exemple, on trouve énormément de microcontrôleurs. Mais avant de les utiliser, il faut les programmer. Durant cette opération, une étape cruciale consiste à écrire le programme sur la mémoire de l’appareil. Pour ça, le développeur branche son ordinateur sur le micro-contrôleur à l’aide d’un câble série. Ensuite deux programmes qui sont sensibles au temps s’exécutent chacun sur l’une des machines. Mais si le temps n’est pas bien maîtrisé, une erreur peut intervenir durant l’écriture. Je voudrais certifier l’exactitude de l’effet temporel des deux programmes : prouver que si l’un s’exécute sur l’ordinateur et l’autre sur le micro-contrôleur, ce dernier se comporte effectivement bien comme on le souhaitait.”
Un autre cas d’usage porterait sur la vérification formelle de librairies de timers dans les systèmes d’exploitation, en particulier pour RIOT, un OS pour l’Internet-des-Objets. “Sur un micro-contrôleur, quand un programme a besoin de connaître le temps, il interroge l’OS qui lui retourne une valeur. Mais peut-on avoir confiance dans cette valeur ? Et d’abord, comment cela fonctionne-t-il ? Et bien en fait, l’OS s’appuie sur deux systèmes. Le premier est un processeur à haute fréquence. Il peut atteindre la micro ou la nanoseconde. Donc très rapide. Mais parfois, il va se décaler dans le temps. Le second est un oscillateur à basse fréquence. Beaucoup plus lent, mais plus précis. Pas de décalage. Un protocole les resynchronise périodiquement. Ce qui génère une source de temps à la fois précise et de haute fréquence. Or, cette resynchronisation, pour l’instant, n’est pas prouvée correcte. Et je voudrais parvenir à le faire.”
Usine numérique
Nommé Cert-t, ce projet va probablement avoir un impact industriel en permettant aux ingénieurs d’augmenter la fiabilité des applications sensibles au temps. En particulier dans le domaine de l’internet des objets, un secteur pour lequel on prévoit un doublement du chiffre d’affaires à l’horizon 2028. À noter aussi que ces travaux de post-doctorat sont supervisés par Jean-Pierre Talpin. Spécialiste des problématiques de temps, ce directeur de recherche Inria collabore avec le constructeur Mitsubishi Electric Europe (MERCE). Le partenariat porte sur la certification de propriétés cyberphysiques de systèmes critiques dans le cadre de ce que l’on appelle désormais les usines numériques.
- L’équipe de développement de CompCert a reçu le prix ACM Software System en 2021.
- Épicure est une équipe-projet Inria, Université de Rennes, ENS Rennes et CNRS, commune à l’Irisa.
