Predicate Diagrams for the Verification of Real-Time Systems

Eunyoung Kang 1 Stephan Merz 1
1 MOSEL - Proof-oriented development of computer-based systems
INRIA Lorraine, LORIA - Laboratoire Lorrain de Recherche en Informatique et ses Applications
Abstract : 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 abstractions. They also represent an interface between deductive tools used to establish 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 is a correct 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 mutual-exclusion protocol.
Keywords : Real-time system verification predicate diagrams theorem proving model checking
Document type :
Conference papers
Complete list of metadatas

Cited literature [22 references]  Display  Hide  Download
https://hal.inria.fr/inria-00000631
Contributor : Eunyoung Kang <>
Submitted on : Thursday, November 10, 2005 - 12:40:13 PM
Last modification on : Thursday, January 11, 2018 - 6:19:52 AM
Long-term archiving on : Friday, April 2, 2010 - 6:55:02 PM

File

final.pdf

Identifiers

  • HAL Id : inria-00000631, version 1

Collections

INRIA | LORIA | UNIV-LORRAINE

Citation

Eunyoung Kang, Stephan Merz. Predicate Diagrams for the Verification of Real-Time Systems. The Fifth International Workshop on Automated Verification of Critical Systems 2005 - AVoCS'05, Ranko Lazic, Rajagopal Nagarajan, Nikolaos Papanikolaou, Sep 2005, Coventry/UK. ⟨inria-00000631⟩

Export

BibTeX TEI DC DCterms EndNote

Share

Metrics

Record views

264

Files downloads

160

Contact


archive-ouverte@inria.fr