Constantin Enea, lauréat d'une ERC Starting Grant

Constantin Enea, maître de conférence et chercheur à l'UFR informatique de Paris Diderot est lauréat d'un ERC Starting Grant qui récompense son travail autour du développement de techniques de vérification formelle et d'analyse pour aider à la construction de systèmes logiciels fiables.

 Augmenter la confiance dans les logiciels repose de manière générale sur des méthodes formelles qui utilisent des langages mathématiques pour exprimer les fonctions attendues des logiciels, et des algorithmes pour les vérifier. Constantin Enea, expert de cette discipline, s’est spécialisé dans une classe particulière de programmes : les structures de données distribuées (DDSs). Ces logiciels, composantes cruciales des systèmes logiciels géo-distribués, maintiennent les données à travers le réseau, s’occupent de les stocker et de les garder toujours accessibles. Ils offrent des fonctions pour l’échange et la consommation de données. C’est par exemple grâce à eux que vous pouvez consulter un document en ligne modifié par un de vos collègues, en étant certain d’avoir la dernière version. L’explosion d’Internet a fait que cette avancée technologique s’est développée trop rapidement, sans que les fondements théoriques puissent être consolidés. Or ces logiciels deviennent de plus en plus critiques, car une information non mise à jour à temps peut avoir des effets conséquents, par exemple dans le domaine bancaire ! C’est là qu’intervient Constantin Enea, afin de vérifier ces programmes.

Deux problèmes principaux se posent avec les DDSs. Tout d’abord, celui de la performance, car il n’est pas acceptable pour un utilisateur d’attendre un « long » moment pour accéder à une information, le temps que le logiciel vérifie en détails qu’il fournit la bonne version. Ensuite, Internet est un immense réseau où des ordres et contre-ordres sur une information peuvent arriver au même moment d’endroits de connexion différents. Il est alors nécessaire de fournir des mécaniques pour résoudre ces conflits entre modifications, afin d’offrir une version consistante des données quel que soit l’endroit d’où on y accède. À cause de ces deux points, les systèmes sont très complexes, et aujourd’hui plus suffisamment maîtrisés au vu de leur utilisation.

Une première étape du projet de Constantin Enea est de définir des spécifications formelles cohérentes qui fournissent des exigences précises au moment de la conception de ces logiciels, et des garanties explicites lors de leur utilisation. D’une part, ces spécifications vont être utilisées pour aider la programmation d’applications « au-dessus » des DDSs, car si ces systèmes assurent les fonctionnalités de base pour faire circuler des données, d’autres fonctionnalités sont nécessaires pour gérer le contexte de ces données. Ce niveau « supérieur » est aujourd’hui très mal maîtrisé, ce qui demandera un travail conséquent sur des principes de programmation et de règles d’utilisation des DDSs.

Ensuite, le projet vise à développer des méthodes automatisées et techniques pour le débogage ou la validation des implémentations des DDSs par rapport à leurs spécifications. Pour cela, il doit tout d’abord définir les limites théoriques du problème de vérification, c’est-à-dire caractériser les classes de systèmes et spécifications où le problème est décidable ou non, et dans le cas où le problème est décidable, établir des résultats de complexité. Pour les cas indécidables, il fournira des outils pratiques pour contourner l’indécidabilité et arriver à une approximation suffisante qui permette de vérifier tout de même le système.