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. © Springer-Verlag Berlin Heidelberg 2000.
CITATION STYLE
Cansell, D., Méry, D., & Merz, S. (2000). Predicate diagrams for the verification of reactive systems. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 1945 LNCS, pp. 380–397). Springer Verlag. https://doi.org/10.1007/3-540-40911-4_22
Mendeley helps you to discover research relevant for your work.