Skip to main content
Kent Academic Repository

Compositional Detection of Zeno Behaviour in Timed Automata

Gomez, Rodolfo and Bowman, Howard (2006) Compositional Detection of Zeno Behaviour in Timed Automata. Technical report. Computing Laboratory, CT2 7NF Canterbury, Kent, UK (KAR id:14389)

Abstract

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.

Item Type: Reports and Papers (Technical report)
Uncontrolled keywords: Zeno, Timed Automata, model-checking
Subjects: Q Science > QA Mathematics (inc Computing science) > QA 76 Software, computer programming,
Divisions: Divisions > Division of Computing, Engineering and Mathematical Sciences > School of Computing
Depositing User: Mark Wheadon
Date Deposited: 24 Nov 2008 18:03 UTC
Last Modified: 16 Nov 2021 09:52 UTC
Resource URI: https://kar.kent.ac.uk/id/eprint/14389 (The current URI for this page, for reference purposes)

University of Kent Author Information

  • Depositors only (login required):

Total unique views for this document in KAR since July 2020. For more details click on the image.