Predicate Diagrams as Basis for the Verification of Reactive Systems

This thesis proposes a diagram-based formalism for verifying
temporal properties of reactive systems. Diagrams integrate
deductive and algorithmic verification techniques for the
verification of finite and infinite-state systems, thus combining
the expressive power and flexibility of deduction with the
automation provided by algorithmic methods. Our formal framework
for the specification and verification of reactive systems includes
the Generalized Temporal Logic of Actions (TLA*) from Merz for both
mathematical modeling reactive systems and specifying temporal
properties to be verified. As verification method we adopt a class
of diagrams, the so-called predicate diagrams from Cansell et al.
We show that the concept of predicate diagrams can be used to
verify not only discrete systems, but also some more complex
classes of reactive systems such as real-time systems and
parameterized systems. We define two variants of predicate
diagrams, namely timed predicate diagrams and parameterized
predicate diagrams, which can be used to verify real-time and
parameterized systems. We prove the completeness of predicate
diagrams and study an approach for the generation of predicate
diagrams. We develop prototype tools that can be used for
supporting the generation of diagrams semi-automatically.