We present an application of partial evaluation to performance models expressed in the PEPA stochastic process algebra . We partially evaluate the state-space of a PEPA model in order to remove uses of the cooperation and hiding operators and compile an arbitrary sub-model into a single sequential component. This transformation is applied to PEPA models which are not in the correct form for the application of the fluid-flow analysis for PEPA . The result of the transformation is a PEPA model which is amenable to fluid-flow analysis but which is strongly equivalent  to the input PEPA model and so, by an application of Hillston’s theorem, performance results computed from one model are valid for the other. We apply the method to a Markovian model of a key distribution centre used to facilitate secure distribution of cryptographic session keys between remote principals communicating over an insecure network.
|Title of host publication||Computer Performance Engineering|
|Subtitle of host publication||5th European Performance Engineering Workshop, EPEW 2008, Palma de Mallorca, Spain, September 24-25, 2008. Proceedings|
|Editors||Nigel Thomas, Carlos Juiz|
|Number of pages||15|
|Publication status||Published - 2008|
|Name||Lecture Notes in Computer Science|
|Publisher||Springer Berlin / Heidelberg|