Skip to Main content Skip to Navigation
Conference papers

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], Inria Saclay - Ile de France
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.
Document type :
Conference papers
Complete list of metadata
Contributor : Stefan Haar Connect in order to contact the contributor
Submitted on : Thursday, January 10, 2013 - 10:56:24 PM
Last modification on : Thursday, February 3, 2022 - 3:43:31 AM

Links full text



Béatrice Bérard, Serge Haddad, Mathieu Sassolas. Real Time Properties for Interrupt Timed Automata. 17th International Symposium on Temporal Representation (TIME 2010), Sep 2010, Paris, France. pp.69-76, ⟨10.1109/TIME.2010.11⟩. ⟨hal-00772673⟩



Record views