An Automatique Technique for CTL* Model Checking

K. Ajami, J.-M. Ilié

LIP6 1997/017: Rapport de Recherche LIP6 / LIP6 research reports
20 pages - Septembre/September 1997 - Document en anglais.

PostScript : 72 Ko /Kb

Contact : par mail / e-mail

Thème/Team: Systèmes Répartis et Coopératifs

Titre français : Une Technique Automatique de Vérification de Propriétés des Systèmes Symétriques
Titre anglais : An Automatique Technique for CTL* Model Checking

Résumé : 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é).

Abstract : In this paper, we propose an automatic technique for CTL* Model checking through the Symbolic Reachability Graph (SRG). SRG is a highly condensed representation of system state space built automatically from a specification of system in terms of Well-formed net. The building of such graph profits from the presence of object symmetries to aggregate either states or actions within symbolic representatives. Our technique consists in making the formal approach of CTL* model checking presented in [1], operational. We propose a derived temporal logic CPN-CTL* (computational Temporal Logic Star) equivalent to CTL* and built to express properties of systems specified by means of a Well-formed net. We show how to perform the model checking of such a formula directly through SRG by retrieving the behavior of the objects specified within these formulas. Effectively, SRG are built according to definitions of representatives of symmetrical object groups for which the identity of objects is not preserved, i.e. only the nature of objects and the cardinality of groups are known. This technique leads to a new specification of system, from which we can prove that model checking through a state space is equivalent to model checking through the symbolic reachability graph.

Mots-clés : Logique Temporelle, CTL*, Symétries,Graphe de Marquages Symboliques, Réseaux de Petri bien formés

Key-words : Temporal Logic, Symmetries, Symbolic Reachability Graph, Well-formed Nets

Publications internes LIP6 1997 / LIP6 research reports 1997

Responsable Éditorial / Editor
webmaster@lip6.fr