Vérification symbolique de modèles à l'aide de systèmes de ré-écriture dédiés
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...
محفوظ في:
| المؤلف الرئيسي: | |
|---|---|
| مؤلفون آخرون: | |
| التنسيق: | Thèse numérique |
| اللغة: | Français |
| منشور في: |
2010.
|
| الموضوعات: | |
| الوصول للمادة أونلاين: | Accès au texte intégral https://theses.univ-orleans.fr/public/2010ORLE2030_vm.pdf http://www.theses.fr/2010ORLE2030/abes https://theses.hal.science/tel-00579490 |
| ملاحظة: |
Thèse soutenue en co-tutelle Titre provenant de l'écran-titre Ecole(s) Doctorale(s) : École doctorale Sciences et technologies (Orléans ; 2009-2012) Partenaire(s) de recherche : Laboratoire d'informatique fondamentale d'Orléans (Orléans ; 1987-....) (Laboratoire), Laboratoire d'Informatique Fondamentale d'Orléans (Laboratoire) Autre(s) contribution(s) : Serge Haddad (Président du jury) ; Jean-Michel Couvreur, Serge Haddad, Didier Buchs, Fabrice Kordon, Yohan Boichut, Ahmed Bouajjani (Membre(s) du jury) ; Didier Buchs, Fabrice Kordon (Rapporteur(s)) |
| Autres localisations: | Voir dans le Sudoc |
| Variante du titre: | Symbolic model-checking based on rewriting systems |
| الملخص: | 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. This PhD thesis proposes the theoretical foundations of a new formal tool for symbolic verification of finite models. Some approaches reduce the problem of system verification to the reachability problem in term rewriting systems (TRSs).In our approach, states are encoded by terms in a BDD-like manner and the transition relation is represented by a new rewriting relation so called Functional Term Rewriting Systems (FTRSs).First, we show that FTRSs are as expressive as TRSs. Then, we focus on a subclass of FTRSs, so called Elementary Functional Term Rewriting Systems (EFTRSs), and we show that EFTRSs preserve the FTRSs expressiveness. The main advantage of EFTRSs is that they are well adapted for acceleration techniques usually used in saturation algorithms on BDD-like data structures.Our experiments show that for well-known protocols (e.g. Tree Arbiter, Percolate, Round RobinMutex protocols,... ) our tool is not only better than other rewriting tools such as Timbuk, Maude or TOM, but also competitive with other model-checkers such as SPIN, NuSMV or SMART. Moreover, it can also be applied to model-checking invariant properties which are a particular subclass of linear temporal logic formula (LTL). |
|---|---|
| وصف المادة: | Thèse soutenue en co-tutelle Titre provenant de l'écran-titre Ecole(s) Doctorale(s) : École doctorale Sciences et technologies (Orléans ; 2009-2012) Partenaire(s) de recherche : Laboratoire d'informatique fondamentale d'Orléans (Orléans ; 1987-....) (Laboratoire), Laboratoire d'Informatique Fondamentale d'Orléans (Laboratoire) Autre(s) contribution(s) : Serge Haddad (Président du jury) ; Jean-Michel Couvreur, Serge Haddad, Didier Buchs, Fabrice Kordon, Yohan Boichut, Ahmed Bouajjani (Membre(s) du jury) ; Didier Buchs, Fabrice Kordon (Rapporteur(s)) |
| التنسيق: | Configuration requise : un logiciel capable de lire un fichier au format : PDF |