Property-dependant bisimulation for compositional model-checking

F. Rahim, E. Encrenaz

LIP6 1997/028: Rapport de Recherche LIP6 / LIP6 research reports
20 pages - Novembre/November 1997 - Document en anglais.

PostScript : 67 Ko /Kb

Contact : par mail / e-mail

Thème/Team: Algorithmique Numérique et Parallélisme

Titre français : Vérification compositionnelle de modèle basée sur une bisimulation dépendant de la propriété
Titre anglais : Property-dependant bisimulation for compositional model-checking

Résumé : es grands systèmes sont généralement modélisés comme une interconnexion de machines d'états finis (FSM). La vérification de modèle de tels systèmes consiste à construire dans un premier temps l'automate produit des composants interconnectés, puis ensuite à parcourir (éventuellement symboliquement) l'espace d'états de cet automate produit. Meme lorsque des représentations symboliques d'espace d'états et de relation de transitions sont utilisées, l'on est rapidement confronté au problème d'explosion combinatoire du nombre d'états du système.
Nous présentons dans ce travail un concept d'équivalence entre états, définie relativement à une propriété CTL à vérifier. Cette équivalence est utilisée pour réduire la taille de l'automate associé à chaque composant élémentaire avant de construire l'automate produit, conduisant ainsi à une réduction de cet automate produit. Contrairement à la bisimulation forte, la relation d'équivalence que nous proposons ne préserve pas toutes les propriétés CTL, et de ce fait l'on construit une équivalence plus grossière entre les états du système, et l'on obtient des taux de réduction plus intéressants. Nous montrons comment appliquer cette approche pour la vérification de propriétés CTL d'entités de programmes VHDL, en adoptant des représentations symboliques basées sur les BDD.

Abstract : Large designs are commonly modelled as a set of interconnected finite state machines (FSM). The basic approach to model checking such designs is to first build the product of the component FSMs and then traverse (e.g. symbolically) this single FSM. Even when using symbolic representations based on BDDs, we have to face the state explosion problem.
We present in this work a concept of state equivalence that is defined with respect to a given CTL formula. This equivalence is used to reduce the size of each component FSM so that their product will be smaller. Contrary of strong bisimulation, it does not preserve all CTL formulae, so we can expect to compute coarser equivalence, inducing a better reduction. We show how to apply this approach using a symbolic representation of the transition relations of VHDL entities in order to check CTL properties.

Mots-clés : vérification formelle, relation d'équivalence, bisimulation, machine d'états finis (FSM), CTL, VHDL

Key-words : formal verification, equivalence relation, bisimulation, finite state machine (FSM), CTL, VHDL

Publications internes LIP6 1997 / LIP6 research reports 1997

Responsable Éditorial / Editor
webmaster@lip6.fr