June 28, 2007 to June 30, 2007
Mani Swaminathan , University of Oldenburg, Germany
Martin Franzle , University of Oldenburg, Germany
DOI Bookmark: http://doi.ieeecomputersociety.org/10.1109/TIME.2007.39
Timed Automata (TA)  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 , 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 , though zone-based, involves a forward and backward fixpoint alternation, and may not necessarily terminate.
Mani Swaminathan, Martin Franzle, "A Symbolic Decision Procedure for Robust Safety of Timed Systems", TIME, 2007, Temporal Representation and Reasoning, International Syposium on, Temporal Representation and Reasoning, International Syposium on 2007, pp. 192, doi:10.1109/TIME.2007.39