Discrete Timed Automata

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.