DeLTA - Défis pour la Logique, les Transducteurs et les Automates

Coordinateur : Marc Zeitoun (Laboratoire Bordelais de Recherche en Informatique)

Équipe : Spirals du Groupe Thématique GL

Partenaires : AMU - LIF Aix-Marseille Université, CNRS, CRIStAL Pierre Bourhis, Chargé de recherche CNRS, IRIF, LaBRI

PRC - Projet de recherche collaborative

Dates : 09/16 - 09/20

Résumé :

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.

Abstract

Software systems are ubiquitous, and more and more complex. The automatedanalysis of computer-generated data and the reliability analysis of complex programs becometherefore crucial, and challenging due to the increasing size and intricacy of the objects thatsoftware systems have to face. Model-checking is a successful technique for system verification,that is now mature, and used for industrial purposes : it amounts to verifying the correctness ofthe system with respect to some specification. The core of this approach relies onfinite-statemachines : on the one hand, they provide an operational model of systems, and on the otherhand, they can be considered as a low-level description of specifications. Finite-state machinesprocessing various kinds of objects, such as words or trees, are very appealing because theycapture one of the most robust concepts in computer science : the notion ofregularity. Thisnotion unifies a triangle (aDelta !) of different approaches with longstanding tradition : anoperational one (automata), a descriptive one (logic), and an equational one (algebra). Logic isa powerful and precise formalism for specifying properties of systems, whereas automata offeran effective algorithmic tool, for instance for verifying and certifying properties ; algebra comesnaturally into play when we ask how far we can go with a specification formalism. The interplaysummarized by the perfect∆of automata-logic-algebra is best understood for languages ofwords, where a rich theory has developed since the fundamental results of the sixties. Sincethen, the theory has grown in many directions, raising new and important challenges.