Nous rappelons tout d'abord le principe des procedures de decision classiques,qui reposent sur des algorithmes de raffinement de partitions. Cette approche necessite de construire au prealable les relations de transition des deux systemes a comparer, ce qui constitue une limitation en pratique. Nous proposons par consequent un algorithme original, base sur un parcours en profondeur du produit synchrone des deux systèmes, qui permet d'effectuer la comparaison ``a la volee'', sans jamais construire ni mémoriser explicitementles deux relations de transition. L'algorithme de comparaison ``a la volée'' a ete mis en œuvre au sein du logiciel de verification Aldebaran dans le cas de différentes relations : la bisimulation forte, l'équivalence observationnelle, la tau*a-bisimulation, la delay bisimulation et la bisimulation de branchement, ainsi que le preordre et l'equivalence de surete. Son application a la verification de plusieurs programmes Lotos de taille realiste a confirme l'interet pratique de notre approche par rapport aux methodes classiques. Enfin, nous nous interessons egalement a la generation d'un diagnostic lorsque les deux systemes de transitions etiquetees a comparer ne sont pas equivalents : les procedures de decision implementees dans Aldebaran fournissent le cas echeant un ensemble de sequences d'execution discriminantes, minimales pour une relation d'ordre donnee.
| Identifer | oai:union.ndltd.org:CCSD/oai:tel.archives-ouvertes.fr:tel-00004729 |
| Date | 31 January 1992 |
| Creators | Mounier, Laurent |
| Source Sets | CCSD theses-EN-ligne, France |
| Language | French |
| Detected Language | French |
| Type | PhD thesis |
Page generated in 0.0028 seconds