L'art de modéliser des systèmes informatiques complexes

Aujourd’hui, nos vies dépendent de plus en plus de systèmes informatiques sophistiqués dans les transports, la santé ou encore la finance. Ces outils pilotent, surveillent et facilitent bien des aspects du quotidien. Mais qui dit complexité, dit aussi risque d’erreurs : un dysfonctionnement dans un avion, un appareil médical qui donne de faux résultats, un réseau qui tombe en panne… Les conséquences peuvent être lourdes, et la fiabilité et la sécurité des systèmes informatiques sont des enjeux essentiels. Mais comment avoir la certitude qu’ils fonctionnent toujours correctement ?

Tester un programme dans toutes les situations imaginables prend beaucoup de temps, et surtout, ce n’est pas suffisant, car il est impossible de prévoir à l’avance chaque cas de figure. C’est pourquoi les chercheurs s’intéressent de plus en plus à la vérification formelle, qui consiste à prouver mathématiquement qu’un programme se comporte comme prévu. Mais encore faut-il avoir les bons outils pour décrire précisément le système et les interactions entre ses composants. C’est pour relever ce défi qu’a été lancé NARCO1 , un projet de recherche en informatique fondamentale, soutenu par l’Agence nationale de la recherche de 2022 à 2026 et coordonné par Nicolas Peltier, chargé de recherche CNRS au Laboratoire d’informatique de Grenoble (LIG)2 .

Modéliser des interactions complexes

« L’un des principes au cœur du projet est la modularité, indique le chercheur, c’est-à-dire qu’au lieu d’analyser un système entier d’un seul bloc, on le décompose ». Chaque module correspond à une partie bien précise du système : un capteur, une base de données, un programme… Cette approche permet de raisonner plus simplement, en étudiant d’abord chaque partie individuellement : les scientifiques identifient les ressources du système, autrement dit ses composants, qui peuvent être physiques (comme un capteur, une batterie ou un circuit) ou logiques (comme un logiciel, une fonction, une règle de décision).

Puis, ils décrivent comment ces ressources interagissent : elles peuvent partager des données, s’influencer mutuellement, se coordonner… C’est ce qu’on appelle la composition du système. Pour qu’elle fonctionne, il faut définir des règles précises d’interaction entre les modules : on parle d’opérateurs de composition.

« Dans les approches classiques, on utilise souvent une union disjointe de structures, c’est-à-dire qu’on assemble les composants comme des blocs indépendants. Ce modèle est simple, mais il ne reflète pas la réalité de nombreux systèmes », relève Nicolas Peltier. En effet, les composants peuvent partager des informations, agir en parallèle ou se coordonner. Par exemple, deux programmes peuvent utiliser ou modifier les mêmes données.

Pour dépasser cette limite, le projet Narco s’appuie sur une approche plus souple, dite de composition non-agrégative : « au lieu de se contenter de juxtaposer les différentes parties, on tient compte de la manière dont celles-ci s’imbriquent et interagissent », explique le chercheur. L’idée est de modéliser les échanges, les dépendances et les partages entre les composants.

Pour décrire rigoureusement ces fonctionnements complexes, les chercheurs s’appuient sur des logiques de séparation, un outil issu de l’informatique théorique. Professeur des universités au Laboratoire lorrain de Recherche en Informatique et ses Applications (Loria), Didier Galmiche travaille sur ces questions depuis plusieurs années. « À l’origine, rappelle-t-il, les logiques de séparation ont été développées pour analyser comment la mémoire est utilisée par différents programmes, en précisant par exemple que chaque programme utilise une partie distincte de la mémoire sans interférer avec les autres. »

Dans le projet NARCO, ces logiques sont adaptées et étendues pour représenter toutes sortes de ressources, ainsi que leur évolution dans le temps : architectures matérielles ou logicielles, données, ou même permissions d’accès. Cela permet de modéliser des systèmes complexes de manière plus fidèle, en tenant compte des interactions réelles entre les différentes parties. Une telle approche rend les modèles créés plus expressifs, au sens où ils sont capables de représenter une plus grande variété de situations et de comportements, comme dans le cas d’un système où plusieurs utilisateurs accèdent en parallèle aux mêmes données. Il s’agit alors de développer des programmes capables d’analyser automatiquement ces modèles pour en vérifier les propriétés.

Des avancées théoriques prometteuses

Cependant, plus un modèle est expressif, plus il est difficile à manipuler, ce qui soulève des défis en termes de complétude puisqu’il faut que les outils puissent démontrer toutes les propriétés attendues. Autres paramètres à prendre en compte : la complexité, c’est-à-dire le coût de l’analyse en temps de calcul et en mémoire, ainsi que l’optimalité qui vise à trouver des solutions à la fois fiables et économes, en minimisant les ressources utilisées. Or, ces trois exigences se retrouvent souvent en tension. « Il faut trouver le bon équilibre : gagner en expressivité sans perdre en rigueur ni en efficacité », résume Nicolas Peltier pour qui « sortir des logiques classiques soulève des défis théoriques ardus, mais stimulants ».

L’objectif est ainsi de créer des outils permettant de vérifier des propriétés importantes du système : par exemple, est-ce que la structure d’un système est bien conforme à sa spécification ? Que se passe-t-il si l’on remplace un composant ? Est-ce que l’ensemble continue de fonctionner comme prévu ? Comment prouver qu’il ne peut pas se produire de conflit ? Des questions primordiales quand le système évolue après une mise à jour logicielle, l’ajout d’un nouveau composant ou un changement dans les règles de fonctionnement.

Pour l’heure, « le projet a donné lieu à une quarantaine de publications », se réjouit Nicolas Peltier. Dans un monde où la technologie influence tous les aspects de nos vies et où les actes de malveillance ont tendance à croître, ces recherches sont essentielles pour développer des systèmes informatiques sécurisés et fiables. En particulier, elles permettent d’étudier des systèmes connectés entre eux, capables de s’adapter si leur organisation évolue alors même qu’ils sont en train de fonctionner.

À plus long terme, elles pourraient être utiles dans d’autres domaines comme celui des cryptomonnaies : la finance décentralisée utilise déjà des logiques de séparation pour éviter les erreurs ou les fraudes et garantir, par exemple, qu’un prélèvement ne dépasse pas le montant autorisé, même lorsque plusieurs transactions sont effectuées en parallèle. Un autre domaine est celui de l’informatique quantique, où les états peuvent parfois être décomposés en sous-parties indépendantes, ne partageant pas de corrélations quantiques. Si les perspectives d’application restent lointaines, les scientifiques entendent bâtir des fondations solides pour mieux comprendre, construire et vérifier des systèmes informatiques complexes.

• 1NARCO. Compositions non-agrégatives de resources
• 2Partenaires du projet NARCO _ Laboratoire d’informatique de Grenoble (LIG - CNRS / UGA / Grenoble INP -UGA / Inria), Verimag (CNRS / UGA), Laboratoire lorrain de recherche en Informatique et ses applications (LORIA - CNRS / Université de Lorraine / CentraleSupélec / Inria) et le Laboratoire Méthodes Formelles (LMF - CNRS / École normale supérieure Paris-Saclay / Université Paris-Saclay).

Ces recherches ont été financées en tout ou partie, par l’Agence nationale de la recherche (ANR) au titre du projet ANR - NARCO - AAPG21. Cette communication est réalisée et financée dans le cadre de l’appel à projet Sciences Avec et Pour la Société - Culture Scientifique Technique et Industrielle pour les projets JCJC et PRC des appels à projets génériques 2021 (SAPS-CSTI-JCJC et PRC AAPG 21).