Time: Wednesday 6.9.2006, 14:30
Place: Room A4-106, Fr. Bajersvej 7
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.