Mani Swaminathan

Oldenburg University, Germany.

Time: Wednesday 6.9.2006, 14:30
Place: Room A4-106, Fr. Bajersvej 7

Robust Zone-Based Forward Reachability Analysis of Timed Automata

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, where termination is enforced by widening. This has however been shown to be in-exact for TA with diagonal constraints that find application in modelling real-time scheduling problems. Recent attempts to deal with TA featuring diagonal constraints, do not, however, consider realistic models that are robust w.r.t modelling errors such as clock-drift, while those that incorporate such robustness (largely for only diagonal-free TA) do not implement a strict zone-based FRA. We present here a zone-based FRA algorithm that is (conjectured to be) exact for TA with diagonal constraints, and robust w.r.t clock-drift, as a step towards efficient verification of a general and realistic class of timed sytems. We then intend to implement these techniques in the model-checker UPPAAL, and extend them to hybrid systems.