DÉfis pour la Logique, les Transducteurs et les Automates – DELTA

Les systèmes logiciels sont omniprésents et de plus en plus complexes. L'analyse automatique de données générées par ceux-ci et leur fiabilité sont ainsi devenues cruciales, et représentent un défi en raison de la taille et de la complexité croissantes des objets manipulés. Le model-checking, domaine mature et utilisé à des fins industrielles, a permis des avancées majeures dans la vérification de la correction d'un système vis-à-vis d'une spécification. Le cœur de cette approche repose sur les machines finies; elles fournissent un modèle opérationnel pour les systèmes et offrent une possibilité de description de spécifications à bas niveau. De telles machines, qui peuvent traiter différents types d'objets (tels que des mots ou des arbres), sont très attrayantes puisqu'elles capturent un des concepts les plus robustes en informatique : la notion de régularité. Cette notion définit un triangle (un Delta !) entre différentes approches bien établies : opérationnelle (automates), descriptive (logique) et équationnelle (algèbre). La logique est un formalisme précis et puissant pour spécifier les propriétés d'un système alors que les automates offrent un outil algorithmique effectif, par exemple pour certifier des propriétés ; l'algèbre, quant à elle, sert à tracer les limites inhérentes d'un formalisme de spécification. L'interaction résumée par ce Delta est bien comprise pour des langages de mots, où une riche théorie a été développée depuis les résultats fondamentaux des années 60. Depuis, la théorie s'est élargie dans de nombreuses directions, créant ainsi de nouveaux et importants défis.

La modélisation via des machines finies est suffisante pour des programmes très simples, dans lesquels les variables prennent leurs valeurs dans un domaine fini. Mais la plupart des systèmes réalistes requièrent de traiter des domaines non bornés. Motivons ainsi les nouvelles difficultés sur trois exemples dans lesquels les domaines finis ne sont plus suffisants. Lors de la modélisation de logiciels embarqués, les valeurs peuvent représenter un niveau d'énergie du système et l'on peut être intéressé par mesurer la consommation maximale ou moyenne en énergie : on doit alors raisonner sur des quantités. Rechercher un motif textuel dans une boîte email peut être résolu efficacement grâce aux automates finis, mais qu'en est-il de la recherche de motifs où on doit comparer certaines valeurs, telles que l'horodatage ou des identifiants de processeurs ? On doit alors raisonner sur des valeurs issues d'un domaine infini. Un dernier exemple est la vérification de programmes traitant des flux de données et qui auraient pour objectif de filtrer à la volée un flot d'éléments pertinents issus d'une séquence d'événements en entrée : la difficulté provient là encore des données non bornées et des besoins en mémoire pour stocker les flots.

De nouvelles théories sont à concevoir pour résoudre ces nouveaux problèmes. Le challenge consiste à conserver tous les avantages de la théorie classique, en particulier en terme de simplicité et d'efficacité des machines finies, tout en gérant des valeurs d'un domaine non borné conformément aux besoins des motivations précédentes. Le projet DELTA propose une recherche fondamentale motivée par la vérification automatique et l'analyse statique de bases de données. Notre objectif premier est d'étendre ces connexions entre automates, logique et algèbre dans des contextes plus riches qui peuvent gérer des valeurs, avec les deux buts suivants :

1. Développer des modèles appropriés pour les trois facettes du Delta, dans les trois extensions considérées : valeurs quantitatives, documents avec données, programmes traitant des flux de données (aussi appelés transducteurs).

2. Gérer efficacement les modèles descriptifs et opérationnels, par exemple en simplifiant des spécifications et des machines, ou en traduisant des spécifications haut niveau en machines bas niveau.