Gomez, Rodolfo and Bowman, Howard
Compositional Detection of Zeno Behaviour in Timed Automata.
Computing Laboratory, CT2 7NF Canterbury, Kent, UK
(Full text available)
The formal specification and verification of real-time systems are difficult tasks, given the complexity of these systems and the safety-critical role they usually play. Timed Automata, and real-time model-checking, have emerged as powerful tools to deal with this problem. However, the specification of urgency in timed automata (essential in most models of interest) may inadvertently cause anomalous behaviours that undermine the reliability of formal verification methods (such as reachability analysis). Zeno runs denote executions which may be arbitrarily fast, i.e., executions where an infinite number of events may occur in a finite period of time. Timelocks denote states where no further divergent execution is possible; i.e., where time cannot pass beyond a certain bound. In general, the verification of safety and liveness properties may be meaningless in models where Zeno runs and timelocks may occur, hence the importance of methods to ensure that models are free from such anomalous behaviours. In previous work, we developed methods to detect Zeno runs and Zeno-timelocks (a particular kind of timelocks) in network of timed automata. Later stages of this analysis derived, from the network's product automaton, reachability formulae that characterise the occurrence of Zeno runs and Zeno-timelocks. Although this simple reachability analysis has a number of advantages over liveness checks (as done in model-checkers such as Uppaal, Kronos and Red), the product automaton is prone to state explosion and so the analysis may not scale well. Here, we refine our previous results by showing that Zeno runs and Zeno timelocks can be characterised by reachability formulae derived from the network's components, i.e., avoiding the product automaton construction.
- Depositors only (login required):