Predicate diagrams for the verification of reactive systems

Dominique Cansell 1 Dominique Méry 1 Stephan Merz
1 MODEL - MODEL (Méthodes formelles et applications)
LORIA - Laboratoire Lorrain de Recherche en Informatique et ses Applications
Abstract : We define a class of diagrams that represent abstractions of---possibly infinite-state---reactive systems described by specifications written in temporal logic. Our diagrams are intended as the basis for the verification of both safety and liveness properties of such systems. Non-temporal proof obligations establish the correspondence between the original specification and the diagram, whereas model checking can be used to verify properties over finite-state abstractions. We describe the use of abstract interpretation techniques to generate proof diagrams from a given specification and user-defined predicates that represent sets of states.
Type de document :
Communication dans un congrès
W. Grieskamp, T. Santen, B. Stoddart. Second International Conference on Integrated Formal Methods - IFM'2000, 2000, Dagstuhl Castle, Germany, Springer-Verlag, 1945, pp.380-397, 2000, Lecture Notes in Computer Science
Liste complète des métadonnées

https://hal.inria.fr/inria-00099125
Contributeur : Publications Loria <>
Soumis le : mardi 26 septembre 2006 - 08:51:08
Dernière modification le : mardi 24 avril 2018 - 13:34:50

Identifiants

  • HAL Id : inria-00099125, version 1

Collections

Citation

Dominique Cansell, Dominique Méry, Stephan Merz. Predicate diagrams for the verification of reactive systems. W. Grieskamp, T. Santen, B. Stoddart. Second International Conference on Integrated Formal Methods - IFM'2000, 2000, Dagstuhl Castle, Germany, Springer-Verlag, 1945, pp.380-397, 2000, Lecture Notes in Computer Science. 〈inria-00099125〉

Partager

Métriques

Consultations de la notice

121