Predicate Diagrams for the Verification of Reactive Systems

Dominique Cansell, Dominique Méry, Stephan Merz

Abstract

We define a class of predicate 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.

© Springer-Verlag

Available as:  gzip'ed Postscript

Reference

@InProceedings{cansell:predicate,
  author =    {Dominique Cansell and Dominique M{\'e}ry
               and Stephan Merz},
  title =     {Predicate Diagrams for the Verification 
               of Reactive Systems},
  booktitle = {2nd Intl. Conf. Integrated Formal Methods (IFM 2000)},
  year =      2000,
  volume =    1945,
  series =    {Lecture Notes in Computer Science},
  address =   {Dagstuhl, Germany},
  month =     nov,
  publisher = {Springer-Verlag},
  pages =     {380--397}
}