© University of Kent - Contact | Feedback | Legal | FOI | Cookies
Specification and analysis of automata-based designs
Jeremy Bryans, Lynne Blair, Howard Bowman, and John Derrick
In W. Grieskamp, T. Stanten, and B. Stoddart, editors, Integrated Formal Methods (IFM 2000), volume 1945 of Lecture Notes in Comuter Science, pages 182-196. Springer, November 2000.Abstract
One of the results of research into formal system specification has been the large number of notations which have been developed. Of these notations, automata have emerged as a promising vehicle for the specification, and particularly the analysis, of systems. This is especially so when the systems under consideration include timing requirements, and timed automata model such systems as a finite set of states with timed transitions between them. However, not all specifications involve deterministic timing, and stochastic automata can be used in these circumstances.
In this paper we consider both timed and stochastic automata, and demonstrate how they can be used in the same design. We will also consider what analysis of the specification can then be performed. In particular, we will describe how to translate stochastic to timed automata, and look at two approaches to model checking the stochastic components of an integrated design.
Download publication 288 kbytes (PostScript)Bibtex Record
@inproceedings{1132,
author = {Jeremy Bryans and Lynne Blair and Howard Bowman and John Derrick},
title = {Specification and Analysis of Automata-based Designs},
month = {November},
year = {2000},
pages = {182-196},
keywords = {determinacy analysis, Craig interpolants},
note = {},
doi = {},
url = {http://www.cs.kent.ac.uk/pubs/2000/1132},
booktitle = {Integrated Formal Methods (IFM 2000)},
editor = {W. Grieskamp and T. Stanten and B. Stoddart},
publication_type = {inproceedings},
publisher = {Springer},
series = {Lecture Notes in Comuter Science},
submission_id = {25201_974464717},
volume = {1945},
}