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 : This article discusses a new 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 modelling 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 article is to extend the format of predicate diagrams to timed systems. We 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; these verification conditions can often be discharged with SMT solvers such as CVC-lite. Additionally, we describe how this approach extends naturally to the verification of parameterized systems. The formalism is supported by a toolkit, and we demonstrate its use at the hand of Fischer's real-time mutual-exclusion protocol.
Type de document :
Article dans une revue
Formal Aspects of Computing, Springer Verlag, 2007, 19 (3), pp.401-413. 〈10.1007/s00165-007-0030-y〉
Liste complète des métadonnées

Littérature citée [27 références]  Voir  Masquer  Télécharger

https://hal.inria.fr/inria-00112065
Contributeur : Eunyoung Kang <>
Soumis le : mercredi 8 novembre 2006 - 10:22:46
Dernière modification le : jeudi 11 janvier 2018 - 06:19:52
Document(s) archivé(s) le : mardi 6 avril 2010 - 21:42:46

Fichier

Identifiants

Collections

Citation

Eunyoung Kang, Stephan Merz. Predicate Diagrams for the Verification of Real-Time Systems. Formal Aspects of Computing, Springer Verlag, 2007, 19 (3), pp.401-413. 〈10.1007/s00165-007-0030-y〉. 〈inria-00112065〉

Partager

Métriques

Consultations de la notice

231

Téléchargements de fichiers

110