loading...
A Symbolic Decision Procedure for Robust Safety of Timed Systems
Alicante, Spain June 28-June 30
DOI Bookmark: http://doi.ieeecomputersociety.org/10.1109/TIME.2007.3914th International Symposium on Tempo ...
 This Article 
 
PURCHASE ARTICLE: $0
HTML
 
 Share 
   
 Bibliographic References 
   
 Add to: 
 
Digg
Furl
Spurl
Blink
Simpy
Google
Del.icio.us
Y!MyWeb
 
 Search 
   
Mani Swaminathan, University of Oldenburg, Germany
Martin Franzle, University of Oldenburg, Germany
Timed Automata (TA) [1] have emerged as an important formalism for the formal modelling and analysis of timed systems. Reachability analysis forms the core of TA-based verification tools such as UPPAAL [2], which implement a zone-based Forward Reachability Analysis (FRA) algorithm. This analysis, however, does not consider realistic models that are robust w.r.t imprecisions such as drift in the clocks. On the other hand, existing techniques for "robust" reachability analysis of TA [3, 4, 5], which deal with such imprecisions, are not straight-forward to implement. The approaches in [3, 4] are region-based, while that of [5], though zone-based, involves a forward and backward fixpoint alternation, and may not necessarily terminate.
Citation:
Mani Swaminathan, Martin Franzle, "A Symbolic Decision Procedure for Robust Safety of Timed Systems," time, pp.192, 14th International Symposium on Temporal Representation and Reasoning (TIME'07), 2007
Usage of this product signifies your acceptance of the Terms of Use.