Real Time Properties for Interrupt Timed Automata

Béatrice Bérard 1 Serge Haddad 2 Mathieu Sassolas 1
1 MoVe - Modélisation et Vérification
LIP6 - Laboratoire d'Informatique de Paris 6
2 MEXICO - Modeling and Exploitation of Interaction and Concurrency
LSV - Laboratoire Spécification et Vérification [Cachan], ENS Cachan - École normale supérieure - Cachan, Inria Saclay - Ile de France, CNRS - Centre National de la Recherche Scientifique : UMR8643
Abstract : Interrupt Timed Automata (ITA) have been introduced to model multi-task systems with interruptions. They form a subclass of stopwatch automata, where the real valued variables (with rate 0 or 1) are organized along priority levels. While reachability is undecidable with usual stopwatches, the problem was proved decidable for ITA. In this work, after giving answers to some questions left open about expressiveness, closure, and complexity for ITA, our main purpose is to investigate the verification of real time properties over ITA. While we prove that model checking a variant of the timed logic TCTL is undecidable, we nevertheless give model checking procedures for two relevant fragments of this logic: one where formulas contain only model clocks and another one where formulas have a single external clock.
Type de document :
Communication dans un congrès
Markey, Nicolas and Wijsen, Jef. 17th International Symposium on Temporal Representation (TIME 2010), Sep 2010, Paris, France. IEEE Computer Society Press, pp.69-76, 2010, 〈10.1109/TIME.2010.11〉
Liste complète des métadonnées

https://hal.inria.fr/hal-00772673
Contributeur : Stefan Haar <>
Soumis le : jeudi 10 janvier 2013 - 22:56:24
Dernière modification le : jeudi 22 novembre 2018 - 14:15:44

Lien texte intégral

Identifiants

Citation

Béatrice Bérard, Serge Haddad, Mathieu Sassolas. Real Time Properties for Interrupt Timed Automata. Markey, Nicolas and Wijsen, Jef. 17th International Symposium on Temporal Representation (TIME 2010), Sep 2010, Paris, France. IEEE Computer Society Press, pp.69-76, 2010, 〈10.1109/TIME.2010.11〉. 〈hal-00772673〉

Partager

Métriques

Consultations de la notice

203