Intitulée : Vérification formelle des systèmes distribués concurrents
Présenté par : Sawsen KHLIFA
Comité de thèse
|
Président
|
Sadok EL ASMI |
Professeur à SUP’COM, Université de Carthage |
|
Rapporteur 1 |
M. Abderrazak JEMAI |
Professur à l’Institut National des Sciences Appliquées et de Technologie |
|
Rapporteur 2 |
M. Heithem ABBES |
Maitre assistant à la Facultés des sciences de Tunis |
|
Examinateur |
M. Neji YOUSSEF |
Professeur à SUP’COM, Université de Carthage |
|
Directrice de thèse |
Mme Asma BEN LETAIFA |
Maître de conférences à SUP’COM, Université de Carthage |
Resumé
La vérification formelle des systèmes concurrents et distribués repose largement sur le model checking, mais cette technique est confrontée au problème majeur de l’explosion combinatoire de l’espace d’états. Lorsque le nombre de composants interagissant augmente, l’espace global croît exponentiellement, rendant l’exploration exhaustive coûteuse, voire impraticable.
Pour répondre à ce défi, cette thèse propose la Structure d’État Réduite Distribuée (RDSS), une nouvelle structure adaptée aux systèmes modulaires modélisés par des réseaux de Petri. La RDSS s’appuie sur la structure DSS tout en éliminant les redondances grâce à une abstraction par transitions silencieuses τ et un mécanisme de fusion dynamique des méta-états. Des preuves formelles garantissent la préservation des comportements globaux et des propriétés temporelles. Deux algorithmes complémentaires ont été développés : une construction séquentielle en C++ démontrant la faisabilité et l’efficacité de l’approche, et une version distribuée implémentée sous ROS 2, exploitant une architecture publish/subscribe pour répartir mémoire et calcul. Le RDSS permet également une vérification efficace de propriétés locales, via la notion de sync-fermeture, incluant la détection de blocages, l’analyse de vivacité et la vérification de propriétés LTL\X.
L’approche est validée sur deux études de cas : un système M2M agricole et un système de patrouille robotique, montrant une réduction significative du nombre de méta-états et d’arcs de synchronisation par rapport à une exploration globale avec LTSmin. Les résultats expérimentaux confirment que la RDSS atténue efficacement l’explosion d’états et constitue une base solide pour la vérification évolutive de systèmes modulaires à grande échelle
Mots-clés Model checking, explosion de l’espace des états, réseaux de Petri modulaires, systèmes distribués, sync-fermeture, TL\X.
Maintenant, allez pousser vos propres limites et réussir!