Predicate Diagrams as Basis for the Verification of Reactive Systems

Nugraheni, Cecilia Esti (2004): Predicate Diagrams as Basis for the Verification of Reactive Systems. Dissertation, LMU München: Fakultät für Mathematik, Informatik und Statistik

Abstract

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.

Abstract

In dieser Arbeit schlagen wir einen diagramm-basierten Formalismus für die Verifikation reaktiver Systeme vor. Diagramme integrieren die deduktiven und algorithmischen Techniken zur Verifikation endlicher und unendlicher Systeme, dadurch kombinieren sie die Ausdrucksstärke und die Flexibilität von Deduktion mit der von algoritmischen Methoden unterstützten Automatisierung. Unser Ansatz für Spezifikation und Verifikation reaktiver Systeme schließt die Generalized Temporal Logic of Actions (TLA*) von Merz ein, die für die mathematische Modellierung sowohl reaktiver Systeme als auch ihrer Eigenschaften benutzt wird. Als Methode zur Verifikation wenden wir Prädikaten-diagramme von Cansell et al. an. Wir zeigen, daß das Konzept von Prädikatendiagrammen verwendet werden kann, um nicht nur diskrete Systeme zu verifizieren, sondern auch kompliziertere Klassen von reaktiven Systemen wie Realzeitsysteme und parametrisierte Systeme. Wir definieren zwei Varianten von Prädikatendiagrammen, nämlich gezeitete Prädikatendiagramme und parametrisierte Prädikatendiagramme, die benutzt werden können, um die Realzeit- und parametrisierten Systeme zu verifizieren. Die Vollständigkeit der Prädikatendiagramme wird nachgewiesen und ein Ansatz für die Generierung von Prädikatendiagrammen wird studiert. Wir entwickeln prototypische Werkzeuge, die die semi-automatische Generierung von Diagrammen unterstützen.

• Dokumententyp: Dissertationen (Dissertation, LMU München)
• Keywords: Formal method, temporal logics, verification, reactive systems, predicate diagrams
• Themengebiete: 500 Naturwissenschaften und Mathematik ; 500 Naturwissenschaften und Mathematik > 510 Mathematik
• Fakultäten: Fakultät für Mathematik, Informatik und Statistik
• Sprache der Hochschulschrift: Englisch
• Datum der mündlichen Prüfung: 13. Februar 2004