Home > Research > Publications & Outputs > Specification and analysis of automata-based de...

Links

Text available via DOI:

View graph of relations

Specification and analysis of automata-based designs

Research output: Contribution in Book/Report/Proceedings - With ISBN/ISSNConference contribution/Paperpeer-review

Published
Close
Publication date1/12/2000
Host publicationIntegrated Formal Methods - Second International Conference, IFM 2000, Proceedings
PublisherSpringer
Pages176-193
Number of pages18
ISBN (print)3540411968, 9783540411963
<mark>Original language</mark>English
Event2nd International Conference on Integrated Formal Methods, IFM 2000 - Dagstuhl Castle, Germany
Duration: 1/11/20003/11/2000

Conference

Conference2nd International Conference on Integrated Formal Methods, IFM 2000
Country/TerritoryGermany
CityDagstuhl Castle
Period1/11/003/11/00

Publication series

NameLecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
Volume1945 LNCS
ISSN (Print)0302-9743
ISSN (electronic)1611-3349

Conference

Conference2nd International Conference on Integrated Formal Methods, IFM 2000
Country/TerritoryGermany
CityDagstuhl Castle
Period1/11/003/11/00

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.