Skip to main content
Kent Academic Repository

Stochastic specification and verification

Bryans, Jeremy W., Derrick, John (1999) Stochastic specification and verification. In: 3rd Irish Workshop in Formal Methods. Electronic Workshops in Computing . Springer (KAR id:21797)


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.

Item Type: Conference or workshop item (Paper)
Uncontrolled keywords: stochastic automata; distributed systems; timed automata; timed automata with deadlines
Subjects: Q Science > QA Mathematics (inc Computing science) > QA 76 Software, computer programming,
Divisions: Divisions > Division of Computing, Engineering and Mathematical Sciences > School of Computing
Depositing User: Mark Wheadon
Date Deposited: 06 Oct 2009 17:37 UTC
Last Modified: 16 Nov 2021 10:00 UTC
Resource URI: (The current URI for this page, for reference purposes)

University of Kent Author Information

Derrick, John.

Creator's ORCID:
CReDIT Contributor Roles:
  • Depositors only (login required):

Total unique views for this document in KAR since July 2020. For more details click on the image.