LIP6 1997/028
- Rapports de recherche
Vérification compositionnelle de modèle basée sur une bisimulation dépendant de la propriété - F. Rahim, E. Encrenaz
- 20 pages - 12/11/1997- document en - http://www.lip6.fr/lip6/reports/1997/lip6.1997.028.ps.gz - 69 Ko
- Contact : Emmanuelle.Encrenaz (at) nulllip6.fr
- Ancien Thème : ANP
- Mots clés : vérification formelle, relation d'équivalence, bisimulation, machine d'états finis (FSM), CTL, VHDL
- Directeur de la publication : Emmanuelle.Encrenaz (at) nulllip6.fr
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.
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.