Skip to main content

Discrete Timed Automata

Gomez, Rodolfo and Bowman, Howard (2005) Discrete Timed Automata. Technical report. UKC (KAR id:14362)

Language: English
Download (464kB) Preview
[thumbnail of TR305.pdf]
This file may not be suitable for users of assistive technology.
Request an accessible format


MONA implements an efficient decision procedure for the logic WS1S, and has already been applied in many non-trivial problems. Among these, we follow on from previous work done by Smith and Klarlund on the verification of a sliding-window protocol. One of the goals of this paper is to extend the scope of MONA to the verification of time-dependent protocols. We present Discrete Timed Automata (DTA) as a suitable formalism to specify and verify such protocols, and (discrete, infinite-state) real-time systems in general. DTA are as much influenced by IO Automata (syntactically) as they are by Timed Automata (semantically). However, DTA presents a number of distinctive features. Among them, urgency conditions can be directly related to actions, and they are constrained in such a way that time-actionlocks are ruled out by construction. A composition strategy is given to combine a set of synchronising automata, resulting in a product automaton over which safety properties can be verified. Invariance proofs are then performed inductively on the automaton structure, and mechanically assisted by MONA. Therefore, this paper also aims to study benefits and weaknesses of DTA as a real-time formalism, compared with existent frameworks such as Timed IO Automata, TLA+ and Clocked Transition Systems. Our case study will be the specification and verification of a multimedia stream protocol. This is compared to previous work where the formalisation of the protocol is realised in UPPAAL.

Item Type: Monograph (Technical report)
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: (The current URI for this page, for reference purposes)
Bowman, Howard:
  • Depositors only (login required):


Downloads per month over past year