DS0702 -

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

Résumé de soumission

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.

Coordinateur du projet

Monsieur Marc Zeitoun (Laboratoire Bordelais de Recherche en Informatique)

L'auteur de ce résumé est le coordinateur du projet, qui est responsable du contenu de ce résumé. L'ANR décline par conséquent toute responsabilité quant à son contenu.

Partenaire

AMU - LIF Aix-Marseille Université - Laboratoire d'Informatique Fondamentale de Marseille
IRIF Institut de Recherche en Informatique Fondamentale
CRIStAL Centre de Recherche en Informatique, Signal et Automatique de Lille
LaBRI Laboratoire Bordelais de Recherche en Informatique

Aide de l'ANR 329 141 euros
Début et durée du projet scientifique : septembre 2016 - 48 Mois

Liens utiles