L'augmentation en taille et en complexité des systèmes réactifs font que leur vérification est de plus en plus difficile à comprendre et à appréhender. Dans cette thèse, une approche est proposée pour spécifier et vérifier compositionnellement certains de ces systèmes.<br /><br />Cette approche est basée sur un principe de décomposition supportant un raffinement compositionnel au niveau des composants et au niveau de leur produit synchronisé~: une méthode est présentée pour vérifier le raffinement d'un système à composants à partir du raffinement de ses composants.<br /><br />Les propriétés LTL sont préservées par le raffinement compositionnel présenté ici. De plus, certaines propriétés -- comme les invariants et les propriétés LTL de sûreté -- peuvent être vérifiées compositionnellement durant la phase de vérification du raffinement.<br /><br />Un outil, nommé SynCo, implante cette approche de vérification compositionnelle. Les différents aspects de ce travail sont illustrés par plusieurs exemples~: un robot industriel, un système d'essuyage et un porte-monnaie électronique.
| Identifer | oai:union.ndltd.org:CCSD/oai:tel.archives-ouvertes.fr:tel-00011649 |
| Date | 31 August 2005 |
| Creators | Lanoix, Arnaud |
| Publisher | Université de Franche-Comté |
| Source Sets | CCSD theses-EN-ligne, France |
| Language | French |
| Detected Language | French |
| Type | PhD thesis |
Page generated in 0.0016 seconds