Vers des outils efficaces pour la vérification de systèmes concurrents

Abstract

Cette thèse cherche à résoudre en pratique le problème de couverture dans les réseaux de Petri et les systèmes de canaux à pertes (LCS). Ces systèmes sont intéressants à étudier car ils permettent de modéliser facilement les systèmes concurrents et les systèmes distribués. Le problème de couverture dans un système de transitions consiste à savoir si on peut, à partir d’un état initial arriver à un état plus grand qu’un état cible. La résolution de ce problème dans les systèmes de transitions bien structurés (WSTS) sera le sujet d’études de la première partie. Les réseaux de Petri et les LCS sont des WSTS. On donnera dans la première partie une méthode générale pour le résoudre rapidement en pratique. Cette méthode utilise des invariants de couverture, qui sont des sur-approximations de l’ensemble des états couvrables. La seconde partie sera consacrée aux réseaux de Petri. Elle présentera diverses comparaisons théoriques et pratiques de différents invariants de couverture. Nous nous intéresserons notamment à la combinaison de l’invariant classique de l’inéquation d’état avec une analyse de signe simple. Les LCS seront le sujet d’études de la troisième partie. On présentera une variante de l’inéquation d’état adaptée aux LCS ainsi que deux invariants qui retiennent des propriétés sur l’ordre dans lequel les messages sont envoyés. La thèse a mené à la création de deux outils, ICover et BML, pour résoudre le problème de couverture respectivement dans les réseaux de Petri et dans les LCS.