Temporal Representation and Reasoning, International Syposium on (2007)
June 28, 2007 to June 30, 2007
DOI Bookmark: http://doi.ieeecomputersociety.org/10.1109/TIME.2007.39
Martin Franzle , University of Oldenburg, Germany
Mani Swaminathan , University of Oldenburg, Germany
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.
Martin Franzle, Mani Swaminathan, "A Symbolic Decision Procedure for Robust Safety of Timed Systems", Temporal Representation and Reasoning, International Syposium on, vol. 00, no. , pp. 192, 2007, doi:10.1109/TIME.2007.39