Cette thèse propose un nouveau type de systèmes de ré-écriture, appelé les systèmes de réécriture fonctionnels. Nous montrons que notre modèle a la puissance d'expression des systèmes de ré-écriture et qu'il est bien adapté à l'étude de propriétés de sûreté et de propriétés de logique temporelle de modèles.Nous avons mis en évidence une sous classe de systèmes fonctionnels, les élémentaires et les élémentaires à droite, préservant la puissance d'expression des systèmes fonctionnels et des techniques d'accélération des calculs aboutissant à un outil de vérification symbolique efficace.Dans la partie expérimentale, nous avons comparé notre outil, d'une part avec des outils de ré-écriture tels que Timbuk, Maude et TOM, d'autre part avec des outils de vérification tels que SPIN, NuSMV, SMART, HSDD. Nos benchmarks démontrent l'efficacité des systèmes fonctionnels élémentaires pour la vérification de modèles.
| Identifer | oai:union.ndltd.org:CCSD/oai:tel.archives-ouvertes.fr:tel-00579490 |
| Date | 21 October 2010 |
| Creators | Nguyên, Duy-Tùng |
| Publisher | Université d'Orléans |
| Source Sets | CCSD theses-EN-ligne, France |
| Language | French |
| Detected Language | French |
| Type | PhD thesis |
Page generated in 0.0015 seconds