KLAI Kais

doctorant à Sorbonne Université
Équipe : MoVe
https://lip6.fr/Kais.Klais

Direction de recherche : Serge HADDAD

Co-encadrement : ILIÉ Jean-Michel

Réseaux de Petri : Vérification Modulaire et Symbolique

La vérification des propriétés des systèmes concurrents est reconnue comme un problème difficile du fait de l’explosion combinatoire des états possibles pour le système. L'objectif de la thèse est d'explorer deux concepts de la littérature permettant de faire face à ce problème. La modularité intrinsèque aux systèmes concurrents d'une part, et la représentation de l'espace d'états accessibles du système en utilisant la structure de diagramme de décision binaire (BDD) d'autre part. La vérification d'une propriété est dite modulaire quand la vérification sur le modèle final se déduit des vérifications de ses composants. Malgré quelques résultats forts du point de vue théorique, la non préservation des propriétés par (dé) composition induit généralement une faible propension à être appliquée à des systèmes réels. Notre idée est de prendre davantage en compte les mécanismes de communication des systèmes pour établir des méthodes reposant sur des conditions d'application plus réalistes. Les approches BDD permettent d'un autre coté, de minimiser l'impact de l'explosion du nombre d'états du système grâce à une représentation des états et des comportements du système particulièrement concise. Le travail effectué dans cette thèse a abouti à trois approches jouant sur des aspects orthogonaux. Dans la première approche, nous abordons la décomposition du réseau de Petri en sous réseaux, tirant profit de synchronisations par fusion de transitions pour préserver le comportement originel. Après avoir corrigé et amélioré le travail de [Souissi91], nous proposons une technique de vérification ramenant la vérification d'une propriété sur le système global à une vérification modulaire sur des parties du système. L'originalité de ce travail réside dans le fait que la procédure de construction des modules étudiés est automatisable en exploitant les propriétés structurelles du modèle global (les invariants du système). Un module est en fait composé d'un sous-réseau complété par une abstraction de son environnement dans le système, de façon à assurer la couverture de l'ensemble des comportements du système global. Sous l'hypothèse d'une non contraignance entre deux modules (dont des conditions effectives de vérification sont donnée), nous assurons la préservation des propriétés de vivacité et du caractère borné ainsi que la préservation des propriétés temporelles validées sur des séquences infinies locales à un sous-réseau (propriétés observationnelles). Dans la deuxième approche présentée dans cette thèse, nous proposons une méthode de vérification purement comportementale. Cette méthode est basée sur la construction d'un graphe réduit à partir de l'observation des actions (transitions) apparaissant dans la formule à vérifier. Les noeuds de ce graphe, dit graphe d'observation, représentent l'abstraction d'un ensemble de marquages liés entre eux par des actions non observées, et les arcs sont exclusivement étiquetés par des actions observées. L'originalité de notre travail réside dans le fait que ce graphe peut être codé de façon très compacte, tirant profit des techniques de représentations symboliques dites BDD (Binary Diagram Decision), tout en préservant le pouvoir de vérification. En effet, la structure du graphe obtenu peut être directement utilisée par les algorithmes classiques de vérification (model-checking) de formules de logique temporelle à temps linéaire. La troisième technique de vérification est une technique fondée sur des heuristiques qui exploitent à la fois la structure du réseau et la propriété à vérifier. Nous proposons une procédure de décision automatisable consistant à définir un sous-système très réduit sur lequel on puisse projeter de façon certaine le processus de vérification d'une propriété de logique temporelle. Dans cette approche, le système est décomposé en deux sous réseaux synchronisés sur un ensemble de transitions : celui supportant la vérification et celui qui représente son environnement. La technique proposée vise, d'une part, à dépasser les limites de notre approche purement structurelles, quand celle-ci fait échec, et d'autre part à exploiter la structure très réduite du graphe d'observation des modules synchronisés.

Soutenance : 01/12/2003

Membres du jury :

Petrucci Laure, (Professeur à Paris 13) [Rapporteur]
Vernadat François, (HDR au LAAS) [Rapporteur]
Haddad Serge, (Professeur à Paris 9)
Ilié Jean-Michel, (Maître de conférences à Paris 5)
Kordon Fabrice, (Professeur à Paris 6)
Barkaoui Kamel, (Professeur au CNAM)

Date de départ : 30/06/2004

Publications 2002-2017