School of Computing

Specification and verification of media constraints using UPPAAL

H. Bowman, G. Faconti, and M. Massink

In 5th Eurographics Workshop on the Design, Specification and Verification of Interactive Systems, DSV-IS 98, Eurographics Series, pages 182-196. Springer-Verlag, August 1998.

Abstract

We present the formal specification and verification of a multimedia stream. The stream is described in a timed automata notation. We verify that the stream satisfies certain quality of service properties, in particular, throughput and end-to-end latency. The verification tool used is the real-time model checker UPPAAL.

Download publication 202 kbytes (PostScript)

Bibtex Record

@inproceedings{576,
author = {H. Bowman and G. Faconti and M. Massink},
title = {Specification and Verification of Media Constraints using {UPPAAL}},
month = {August},
year = {1998},
pages = {182-196},
keywords = {determinacy analysis, Craig interpolants},
note = {},
doi = {},
url = {http://www.cs.kent.ac.uk/pubs/1998/576},
    booktitle = {5th Eurographics Workshop on the Design, Specification and Verification of Interactive Systems, DSV-IS 98},
    publisher = {Springer-Verlag},
    refereed = {yes},
    series = {Eurographics Series},
}

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

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

Last Updated: 21/03/2014