Ahmed Bouajjani : des automates pour vérifier les programmes
Près de 25 ans après sa publication, un article co-rédigé par Ahmed Bouajjani de l’Institut de Recherche en Informatique Fondamentale (IRIF - CNRS/Université de Paris) a été primé à la conférence CONCUR pour son influence sur la vérification de modèles. Ces travaux proposent des algorithmes de vérification de systèmes dits « à pile ». L’approche utilise des automates pour représenter de manière finie et manipuler des ensembles infinis de configurations de systèmes.
Les systèmes informatiques ont besoin d’être inspectés de manière formelle et systématique pour savoir s’ils vont fonctionner correctement. Ahmed Bouajjani, professeur à l’Université de Paris et responsable du pôle Automates, structures et vérification à l’IRIF, explore des problèmes de spécification, de modélisation et de vérification formelle des systèmes. Une grande partie de ses travaux est consacrée aux méthodes de vérification s’apparentant au model checking, ou vérification de modèles, pour différentes classes de systèmes infinis.
« Ma recherche vise à concevoir des méthodes et des outils permettant aux programmeurs d’améliorer la qualité de leurs programmes, notamment en termes de fiabilité, explique Ahmed Bouajjani. Je travaille à la vérification automatique qu’un programme satisfait bien les propriétés qu’il doit satisfaire, puis à la correction des éventuels problèmes. » Parmi les différentes approches, Ahmed Bouajjani s’est spécialisé dans la vérification algorithmique.
Son article fondateur Reachability analysis of pushdown automata: application to model-checking, co-écrit avec Javier Esparza1 et Oded Maler, a reçu le prix Test-of-time de la conférence CONCUR2 2021 après avoir été présenté à la conférence CONCUR… 1997 ! Cette récompense se laisse en effet un long recul pour observer le véritable impact des articles qu’il distingue, avec cette année quatre lauréats pour des travaux publiés entre 1994 et 1999. Ahmed Bouajjani était dans les années 90 membre du laboratoire VERIMAG (CNRS/Université Grenoble Alpes), dirigé à l’époque par Joseph Sifakis, actuellement directeur de recherche CNRS émérite, premier français à obtenir le prix Turing pour ses travaux sur le model checking.
« À l’époque, les travaux sur le model-checking considéraient essentiellement des systèmes avec un nombre fini de configurations possibles, précise Ahmed Bouajjani. Ces modèles ne sont généralement pas assez expressifs pour représenter fidèlement les comportements des systèmes logiciels, et nos travaux ont contribué au passage à des modèles au nombre infini de configurations. Le modèle des systèmes à pile offre assez d’expressivité pour servir à ces applications, tout en étant assez restreint pour conserver de bonnes propriétés algorithmiques. »
Le modèle des systèmes à pile consiste en des machines abstraites possédant un nombre fini d’états de contrôle, et où chaque changement d’état permet de réaliser une opération sur des données structurées en pile. Trois actions sont disponibles : vérifier si la pile est vide, ajouter quelque chose sur la pile ou enlever l’élément en sommet de pile. Dans ces systèmes, la taille de la pile n’est pas bornée et donc peut croître arbitrairement, rendant ainsi le nombre de configurations possibles d’un système à pile infini.
Les automates offrent ainsi une représentation compacte et finie d’ensembles infinis de configurations de pile. Dans les travaux présentés à CONCUR 1997, des algorithmes de model-checking sont définis pour vérifier qu’une certaine propriété exprimée dans un langage logique général est bien satisfaite par un système à pile donné. Plus généralement, grâce à l’approche utilisant les automates, ces algorithmes permettent de calculer l’ensemble des configurations du système qui satisfont la propriété ciblée.
Depuis, Ahmed Bouajjani a exploré de multiples généralisations et applications des automates à pile, ainsi que différentes classes de systèmes informatiques. Ses travaux récents portent sur la concurrence et sur les systèmes distribués, où il faut assurer un certain niveau de consistance entre les données stockées et traitées sur plusieurs machines distantes à la fois.