V. Rusu, M. Clavel. Vérification d'invariants pour des systèmes spécifiés en logique de réécriture. In Vingtièmes Journées Francophones des Langages Applicatifs, JFLA 2009, A. Schmitt (ed.), Studia Informatica Universalis, Volume 7.2, Pages 317-350, Saint Quentin sur Isère, France, February 2009.
Download paper:
Adobe portable document (pdf)
Copyright notice:
This material is presented to ensure timely dissemination of scholarly and
technical work. Copyright and all rights therein are retained by authors or
by other copyright holders. All persons copying this information are expected
to adhere to the terms and constraints invoked by each author's
copyright. These works may not be reposted without the explicit permission of
the copyright holder.
This page is automatically generated by bib2html v216, © INRIA 2002-2007, Projet Lagadic
Nous présentons une approche basée sur la preuve inductive pour vérifier des invariants de systèmes spécifiés en \emph{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 \emph{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 correct, 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.
We present an approach based on inductive theorem proving for verifying invariants of dynamic systems specified in rewriting logic, a formal specification language implemented 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 properties 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 in an n-process Bakery algorithm
Vlad Rusu http://www.irisa.fr/vertecs/Equipe/Rusu/vlad-rusu.html
@InProceedings{RusuC09,
Author = {Rusu, V. and Clavel, M.},
Title = {Vérification d'invariants pour des systèmes spécifiés en logique de réécriture},
BookTitle = {Vingtièmes Journées Francophones des Langages Applicatifs, JFLA 2009},
editor = {Schmitt, A.},
Volume = {7.2},
Pages = {317--350},
Series = {Studia Informatica Universalis},
Address = {Saint Quentin sur Isère, France},
Month = {February},
Year = {2009}
}
Get EndNote Reference (.ref)
|
| VerTeCs
| Team
| Publications
| New Results
| Softwares
|
Irisa - Inria - Copyright 2005 © Projet VerTeCs |