Stochastic Process Algebras - Integrating Qualitative and Quantitative Modelling

J. Hillston, H. Hermanns, U. Herzog, V. Mertsiotakis, M. Rettelbach, H. Hermanns delta U. Herzog, V. Mertsiotakis delta M. Rettelbach

Research output: Chapter in Book/Report/Conference proceedingConference contribution

Abstract

In this paper we present an extension of the process algebra modelling methodology which allows qualitative and quantitative modelling to be integrated. This extension, to form stochastic process algebras (SPA), has been recently demonstrated to have many interesting features. Such languages serve two purposes as a formal description language for computer system models. Quantitative information may be used to predict the performance of the system whereas qualitative information may be exploited when reasoning about the functional behaviour of the system (e.g. when finding deadlocks or when exhibiting equivalences between subcomponents). While qualitative analysis is carried out using standard techniques for process algebras, quantitative analysis is based on an underlying continuous time Markov chain (CTMC). Several stochastic process algebras have recently appeared in the literature. Here we present the emerging concensus of the salient features for such languages and discuss their use for modelling distributed systems. We illustrate these features in an example taken from the field of communication systems. Moreover, standard theoretical results from the area of process algebras, such as establishing congruence relations are shown to have practical applications for modelling, and analysing, large systems.
Original languageEnglish
Title of host publicationProceeding of: Formal Description Techniques VII, Proceedings of the 7th IFIP WG6.1 International Conference on Formal Description Techniques, Berne, Switzerland, 1994
Publication statusPublished - 1994

Fingerprint Dive into the research topics of 'Stochastic Process Algebras - Integrating Qualitative and Quantitative Modelling'. Together they form a unique fingerprint.

Cite this