Portal de Periódicos da CAPES

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

2009; Volume: 7; Issue: 2 Linguagem: Francês

1625-7545

Vlad Rusu, Manuel Clavel,

Advanced Software Engineering Methodologies

Nous presentons une approche basee sur la preuve inductive pour verifier des in- variants de systemes specifies en logique de reecriture, un langage de specification formelle implemente dans l'outil Maude. Un invariant est une propriete qui est vraie dans tous les etats atteignables a partir d'une certaine classe d'etats initiaux. Notre approche consiste a coder les proprietes d'invariance de la logique de reecriture en logique equationnelle avec appartenance, une sous-logique de la logique de reecriture egalement implementee dans Maude. Ce codage nous permet ensuite de prouver les proprietes d'invariance a l'aide d'un assistant de preuve disponible pour la logique equationnelle de Maude. Nous montrons que notre codage est cor- rect, pour un sous-ensemble bien identifie (et suffisant en pratique) de systemes et de proprietes d'invariance, et illustrons notre approche sur une version a n processus de l'algorithme Bakery.