Discrete Timed Automata and MONA: Description, Specification and Verification of a Multimedia Stream

Gomez, Rodolfo and Bowman, Howard (2003) Discrete Timed Automata and MONA: Description, Specification and Verification of a Multimedia Stream. In: Konig, H. and Heiner, M. and Wolisz, A., eds. Lecture Notes in Computr Science. LNCS, 2767 (2767). Springer, Berlin, Germany pp. 177-192. ISBN 3-540-20175-0 . (The full text of this publication is not currently available from this repository. You may be able to access a copy if URLs are provided)

The full text of this publication is not available from this repository. (Contact us about this Publication)
Official URL


MONA implements an efficient decision procedure for the weak second-order logic WS1S, and has already been applied in many non-trivial problems. Among these, we follow on from the work of Smith and Klarlund on the verification of a sliding-window protocol. This paper extends 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. In this paper our case study will be the specification and verification of a multimedia stream. DTA are as much influenced by IO Automata (syntactically) as they are by Timed Automata (semantically). 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. MONA supports the mechanical verification of invariance proofs.

Item Type: Conference or workshop item (UNSPECIFIED)
Subjects: Q Science > QA Mathematics (inc Computing science) > QA 76 Software, computer programming,
Divisions: Faculties > Science Technology and Medical Studies > School of Computing > Theoretical Computing Group
Depositing User: Mark Wheadon
Date Deposited: 24 Nov 2008 18:00
Last Modified: 12 May 2014 14:12
Resource URI: https://kar.kent.ac.uk/id/eprint/13904 (The current URI for this page, for reference purposes)
  • Depositors only (login required):