Vérification d'invariants pour des systèmes spécifiés en logique de réécriture

Résumé : Nous présentons une approche basée sur la preuve inductive pour vérifier des in- variants de systèmes spécifiés en logique de réécriture, un langage de spécification formelle implémenté dans l'outil Maude. Un invariant est une propriété qui est vraie dans tous les états atteignables à partir d'une certaine classe d'états initiaux. Notre approche consiste à coder les propriétés d'invariance de la logique de réécriture en logique équationnelle avec appartenance, une sous-logique de la logique de réécriture également implémentée dans Maude. Ce codage nous permet ensuite de prouver les propriétés d'invariance à l'aide d'un assistant de preuve disponible pour la logique équationnelle de Maude. Nous montrons que notre codage est cor- rect, pour un sous-ensemble bien identifié (et suffisant en pratique) de systèmes et de propriétés d'invariance, et illustrons notre approche sur une version à n processus de l'algorithme Bakery.
Type de document :
Article dans une revue
Studia Informatica Universalis, Hermann, 2009, JFLA 2009, Vingtiemes Journees Francophones des Langages Applicatifs, 7 (2)
Liste complète des métadonnées

Littérature citée [21 références]  Voir  Masquer  Télécharger

https://hal.inria.fr/inria-00564219
Contributeur : Mister Dart <>
Soumis le : mardi 8 février 2011 - 12:59:08
Dernière modification le : mercredi 11 avril 2018 - 01:53:43
Document(s) archivé(s) le : mardi 6 novembre 2012 - 13:40:19

Fichier

rusu.pdf
Fichiers produits par l'(les) auteur(s)

Identifiants

  • HAL Id : inria-00564219, version 1

Collections

Citation

Vlad Rusu, Manuel Clavel. Vérification d'invariants pour des systèmes spécifiés en logique de réécriture. Studia Informatica Universalis, Hermann, 2009, JFLA 2009, Vingtiemes Journees Francophones des Langages Applicatifs, 7 (2). 〈inria-00564219〉

Partager

Métriques

Consultations de la notice

194

Téléchargements de fichiers

158