Predicate Diagrams for the Verification of Real-Time Systems

9 years 10 months ago
Predicate Diagrams for the Verification of Real-Time Systems
We propose a format of predicate diagrams for the verification of real-time systems. We consider systems that are defined as extended timed graphs, a format that combines timed automata and constructs for modeling data, possibly over infinite domains. Predicate diagrams are succinct and intuitive representations of Boolean ions. They also represent an interface between deductive tools used to h the correctness of an abstraction, and model checking tools that can verify behavioral properties of finite-state models. The contribution of this paper is to extend the format of predicate diagrams to timed systems. We also establish a set of verification conditions that are sufficient to prove that a given predicate diagram rect abstraction of an extended timed graph. The formalism is supported by a toolkit, and we demonstrate its use at the hand of Fischer's real-time mutualexclusion protocol. s: Real-time systems, verification, abstraction, XTG, predicate diagrams, theorem proving, mod...
Eun-Young Kang, Stephan Merz
Added 12 Dec 2010
Updated 12 Dec 2010
Type Journal
Year 2006
Authors Eun-Young Kang, Stephan Merz
Comments (0)