Predicate diagrams as basis for the verification of reactive systems

Show simple item record

dc.contributor.advisor Kroger, Fred
dc.contributor.advisor Merz, Stephan
dc.contributor.author Nugraheni, Cecilia Esti
dc.date.accessioned 2017-06-09T07:30:56Z
dc.date.available 2017-06-09T07:30:56Z
dc.date.issued 2004
dc.identifier.uri http://hdl.handle.net/123456789/2225
dc.description.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. en_US
dc.publisher Fakultat fur Mathematik, Informatik und Statistik der Ludwig-Maxmilians-Universitat Munchen en_US
dc.title Predicate diagrams as basis for the verification of reactive systems en_US
dc.type Dissertations en_US


Files in this item

This item appears in the following Collection(s)

Show simple item record

Search UNPAR-IR


Advanced Search

Browse

My Account