LIP6 1997/017
- Rapports de recherche
Une Technique Automatique de Vérification de Propriétés des Systèmes Symétriques - K. Ajami, J.-M. Ilié
- 20 pages - 10/09/1997- document en - http://www.lip6.fr/lip6/reports/1997/lip6.1997.017.ps.gz - 74 Ko
- Contact : Khalil.Ajami (at) nulllip6.fr, Jean-Michel.Ilie (at) nulllip6.fr
- Ancien Thème : SRC
- Mots clés : Logique Temporelle, CTL*, Symétries,Graphe de Marquages Symboliques, Réseaux de Petri bien formés
- Directeur de la publication : Denis.Poitrenaud (at) nulllip6.fr
Dans cet article, nous proposons une technique de vérification des propriétés des systèmes symétriques à partir du graphe de marquages symboliques. Un Graphe de Marquages Symboliques (GMS) est une représentation condensée du graphe d'états construit automatiquement à partir d'une spécification en termes de réseaux colorés. La construction d'un tel graphe utilise les symétries structurelles du système pour agréger les états et les actions entre les états (les transitions) dans des classes d'équivalences en choisissant des représentant des classes pour décrire l'évolution du système. Notre technique consiste à adapter et à utiliser, dans un modèle opérationnel, l'approche formelle, de la vérification des propriétés exprimées en CTL* (computational Temporal Logic Star), proposée par Emerson & al [1]. Nous proposons une logique temporelle CPN-CTL* (computational Temporal Logic Star for Colored Petri Nets), dérivée de CTL* et adaptée syntaxiquement à nos spécifications en termes de réseaux bien formés.Nous montrons, comment la vérification des propriétés peut être réalisée directement, sur le graphe de marquages symboliques malgré sa construction à partir des représentants des classes d'équivalences des états et des transitions. En effet, dans une telle représentation, les identités des objets spécifiés par la formule n'apparaissent pas dans les marquages du graphe, seule une notion de groupe d'objets est préservée indiquant la nature des objets dans le groupe ainsi que sa cardinalité. Cette technique donne lieu à une nouvelle spécification du système permettant la vérification directe des propriétés sur le graphe de marquages symboliques. Cette vérification est équivalente à la vérification des mêmes propriétés sur le graphe d'états ordinaire (graphe d'accessibilité).