Model Checking based on Occurrence Net Graph
J.-M. Couvreur, D. Poitrenaud
Masi-IBP
1996/06: Rapport de Recherche
Masi / Masi
research reports
11 pages - Avril/April 1996 -
Document en anglais.
PostScript :
54 Ko /Kb
Titre français : Graphes de réseaux d'occurrences pour la vérification de modèles
Titre anglais : Model Checking based on Occurrence Net Graph
Résumé : La construction du graphe d'accessibilités est la méthode la plus utilisée pour la vérification des propriétés d'un système. Son inconvénient principal est l'explosion du nombre d'états. Deux approches différentes sont généralement employées pour lutter contre ce problème: définir de nouvelles representations concises du graphe pour lesquelles les méthodes de vérification sont adaptées; réduire le graphe tout en préservant les propriétés à vérifier. Nous proposons une nouvelle représentation des graphes d'accessibilités dans laquelle chaque noeud est un réseau de Petri particulier, un réseau d'occurrences, caractérisant une partie des états accessibles. La vérification de propriétés invariantes peut être réalisée par l'utilisation d'algorithmes efficaces dédiés aux réseaux d'occurrences. De plus, notre représentation peut être utilisée de façon à obtenir un graphe respectant l'équivalence begayante à partir duquel les formules de logique temporelle à temps linéaire (privée de l'opérateur Next) peuvent être vérifiées.
Abstract : The computation of a reachability graph is one of the most used method to check system properties. Its main drawback is the state explosion. Two different approaches are generally used to tackle this problem: to define new concise graph representations for which verification methods are adapted; to reduce graphs while preserving observed properties. We propose a new representation of a reachability graph where nodes are particular Petri nets, occurrence nets, characterizing state space parts. Checking invariant properties can be done using efficient algorithms for occurrence nets. Moreover, our representation can be used to obtain a stuttering equivalent graph on which nexttime-less linear temporal formulas are verified.
Mots-clés : Vérification de systèmes, graphes d'accessibilités, logique temporelle linéaire, équivalence bégayante
Key-words : Model Checking, Reachability Graph, Linear Temporal Logic, Stuttering Equivalence
Publications
internes Masi 1996 /
Masi research reports 1996