Cette thèse propose une nouvelle technique de vérification par model-checking de propriétés dynamiques PLTL, exprimées au cours d'un processus de spécification de systèmes réactifs par raffinement. La vérification par model-checking a l'avantage d'être entièrement automatisable, mais elle se heurte au problème de l'explosion combinatoire de l'espace d'états à vérifier. Afin de faire face à ce problème, nous proposons de découper par partition l'espace d'états en un ensemble de modules, et de mener la vérification successivement sur chacun des modules, afin de pouvoir conclure sur le modèle dans son ensemble. Nous prouvons que cette méthode de vérification (appelée vérification modulaire) est valide pour tout une classe de propriétés PLTL, que nous caractérisons par des automates de Büchi. Nous présentons les systèmes d'événements B comme cadre d'application de cette technique. Nous proposons une méthode de découpage en modules guidée par le processus de raffinement B.
| Identifer | oai:union.ndltd.org:CCSD/oai:tel.archives-ouvertes.fr:tel-00011112 |
| Date | January 2001 |
| Creators | Masson, Pierre-Alain |
| Publisher | Université de Franche-Comté |
| Source Sets | CCSD theses-EN-ligne, France |
| Language | French |
| Detected Language | French |
| Type | PhD thesis |
Page generated in 0.0017 seconds