Specification and Analysis of Automata-based Designs

Bryans, Jeremy W. and Blair, Lynne and Bowman, Howard and Derrick, John (2000) Specification and Analysis of Automata-based Designs. In: Grieskamp, Wolfgang and Stanten, Thomas and Stoddart, Bill, eds. Integrated Formal Methods: Second International Conference, IFM 2000, Dagstuhl Castle, Germany, November 2000. Proceedings. Lecture Notes in Comuter Science, 1945. Springer pp. 176-193. ISBN 3-540-41196-8. (Full text available)

Download (295kB)
Download (272kB)


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.

Item Type: Conference or workshop item (Paper)
Uncontrolled keywords: Timed automata, stochastic automata, model checking.
Subjects: Q Science > QA Mathematics (inc Computing science) > QA 76 Software, computer programming,
Divisions: Faculties > Sciences > School of Computing > Theoretical Computing Group
Faculties > Sciences > School of Computing > Systems Architecture Group
Depositing User: Mark Wheadon
Date Deposited: 13 Sep 2009 18:43 UTC
Last Modified: 18 Jun 2014 10:41 UTC
Resource URI: https://kar.kent.ac.uk/id/eprint/21939 (The current URI for this page, for reference purposes)
  • Depositors only (login required):


Downloads per month over past year