School of Computing

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

Rodolfo Gomez and Howard Bowman

In H Konig, M Heiner, and A Wolisz, editors, Formal Techniques for Networked and Distributed Systems - FORTE 2003. Proceedings of the 23rd IFIP WG 6.1 International Conference, number 2767 in LNCS, pages 182-196, Berlin, Germany, September 2003. Springer.

Abstract

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.

Download publication 214 kbytes (PDF)

Bibtex Record

@inproceedings{1625,
author = {Rodolfo Gomez and Howard Bowman},
title = {Discrete {T}imed {A}utomata and {MONA}: {D}escription, {S}pecification and {V}erification of a {M}ultimedia {S}tream},
month = {September},
year = {2003},
pages = {182-196},
keywords = {determinacy analysis, Craig interpolants},
note = {},
doi = {},
url = {http://www.cs.kent.ac.uk/pubs/2003/1625},
    publication_type = {unpublished},
    submission_id = {7942_1054999518},
    editor = {H Konig and M Heiner and A Wolisz},
    booktitle = {Formal Techniques for Networked and Distributed Systems - FORTE 2003. Proceedings of the 23rd IFIP WG 6.1 International Conference},
    address = {Berlin, Germany},
    number = {2767},
    series = {LNCS},
    publisher = {Springer},
    refereed = {Yes},
}

School of Computing, University of Kent, Canterbury, Kent, CT2 7NF

Enquiries: +44 (0)1227 824180 or contact us.

Last Updated: 21/03/2014