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.
|Title of host publication||Proceeding of: Formal Description Techniques VII, Proceedings of the 7th IFIP WG6.1 International Conference on Formal Description Techniques, Berne, Switzerland, 1994|
|Publication status||Published - 1994|