Vérification d'invariants pour des systèmes spécifiés en logique de réécriture
Résumé
We present an approach based on inductive theorem proving for verifying invari- ants of dynamic systems specified in rewriting logic, a formal specification language imple- mented in the Maude system. An invariant is a property that holds on all the states that are reachable from a given class of initial states. Our approach consists in encoding the semantic aspects that are relevant for our task (namely, verifying invariance properties of the specified systems) in membership equational logic, a sublogic of rewriting logic. The invariance prop- erties are then formalized over the encoded rewrite theories and are proved using an inductive theorem prover for membership equational logic also implemented in the Maude system using its reflective capabilities. We illustrate our approach by verifying mutual exclusion properties of a readers-writers system and of an n-process version of the Bakery algorithm.
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.
Domaines
Systèmes embarqués
Origine : Fichiers produits par l'(les) auteur(s)
Loading...