Direction de recherche : Serge HADDAD

Graphe symbolique paramétré de réseaux de Petri et Logique temporelle

Les programmes parallèles sont souvent définis pour un nombre fini mais non déterminé de processus. On peut alors souhaiter vérifier des propriétés des programmes quel que soit le nombre de processus. Le programme défini pour un nombre fixé de processus est un programme instancié. Il a été prouvé que dans le cas général la vérification paramétrée, i.e. sans fixer le nombre de processus, est un problème indécidable. Cependant, de nombreux travaux ont eu pour but de résoudre ce problème pour des cas particuliers. Les méthodes proposées sont non programmables, semi-décidables, avec des cas d'échec ou imposent des restrictions importantes sur les propriétés et les modèles étudiés. Nous proposons une méthode de vérification paramétrée de programmes parallèles en utilisant une approche nouvelle. Nous représentons de manière symbolique, par un graphe, l'ensemble des évolutions possibles de presque tous les programmes instanciés. Le "presque tous" est dû au fait que le graphe symbolique n'est représentatif des états accessibles d'un programme instancié que si le nombre de processus est supérieur à une borne calculée lors de la construction du graphe. Le graphe symbolique peut être utilisé comme structure de vérification de propriétés. La méthode de vérification paramétrée que nous proposons présente des cas d'échec qui sont détectés par les algorithmes la mettant en oeuvre. Ces cas d'échec sont cohérents avec le fait que le problème que nous souhaitons résoudre est indécidable dans le cas général. Nous avons prouvé que lorsqu'aucun cas d'échec n'est rencontré les algorithmes se terminent en temps fini, le graphe construit représente bien l'ensemble de comportements souhaité et le résultat de la vérification est correct. Nous représentons les programmes par des réseaux de Petri et les propriétés par des formules de logique temporelle de temps arborescent.

Publications 1994-2020