School of Computing

Stochastic specification and verification

Jeremy Bryans and John Derrick

In 3rd Irish Workshop in Formal Methods, Electronic Workshops in Computing, pages 182-196. Springer, July 1999.

Abstract

Modern distributed systems include a class of applications in which non-functional requirements are important. In particular, these applications include multimedia facilities where real time constraints are crucial to their correct functioning. In order to specify such systems it is necessary to describe that events occur at times given by probability distributions. Stochastic process algebras have emerged as a useful technique by which such systems can be specified and verified.

However, stochastic descriptions are very general, in particular they allow the use of general probability distribution functions, and therefore their verification can be complex. In this paper we define a translation from stochastic process algebras to timed automata. By doing so we aim to use the simpler verification methods for timed automata (e.g. reachability properties) for the more complex stochastic descriptions.

Download publication 72 kbytes

Bibtex Record

@inproceedings{818,
author = {Jeremy Bryans and John Derrick},
title = {{S}tochastic specification and verification},
month = {July},
year = {1999},
pages = {182-196},
keywords = {determinacy analysis, Craig interpolants},
note = {},
doi = {},
url = {http://www.cs.kent.ac.uk/pubs/1999/818},
    booktitle = {3rd Irish Workshop in Formal Methods},
    publisher = {Springer},
    refereed = {yes},
    series = {Electronic Workshops in Computing},
}

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

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

Last Updated: 21/03/2014