Stochastic process algebras such as PEPA provide ample support for the component-based construction of models. Tools compute the numerical solution of these models; however, the stochastic process algebra methodology lacks support for the specification and calculation of complex performance measures. This paper addresses that problem by presenting a performance specification language which supports high level reasoning about PEPA models, allowing the description of equilibrium (steady-state) measures. The meaning of the specification language can be made formal by examining its foundations in a stochastic modal logic. A case-study is presented to illustrate the approach.
|Title of host publication||Formal Methods for Real-Time and Probabilistic Systems|
|Subtitle of host publication||5th International AMAST Workshop, ARTS’99 Bamberg, Germany, May 26–28, 1999 Proceedings|
|Number of pages||17|
|Publication status||Published - 1999|
|Name||Lecture Notes in Computer Science|
|Publisher||Springer Berlin / Heidelberg|