Vérification symbolique de modèles : à l'aide de systèmes de ré-écritures dédiés

ISBN-13: 9786131579783 / Francuski / Miękka / 2011 / 200 str.

Duy Tung Nguyen

Opis

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 résultats démontrent l'efficacité des systèmes fonctionnels élémentaires pour la vérification de modèles.

O autorze

NGUYEN, Duy TungÉtant ingénieur en Informatique de l'Institut Polytechnique deHanoï, Vietnam depuis 2002, M NGUYEN Duy Tung continue ses étudesen Master 2 à l'IFI. Après son stage au LaBRI, Univ. Bordeaux Ien 2005, il poursuit une thèse concernant de la vérificationsymbolique basée sur des systèmes de ré-écriture au LIFO, Univ.d'Orléans.