Partial Evaluation of PEPA Models for Fluid-Flow Analysis

Abstract. We present an application of partial evaluation to performance models expressed in the PEPA stochastic process algebra [1]. 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 [2]. The result of the transformation is a PEPA model which is amenable to fluid-flow analysis but which is strongly equivalent [1] 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.

• Type: Conference
• Year: 2008
• Where: EPEW
• Authors: Allan Clark, Adam Duguid, Stephen Gilmore, Mirco Tribastone
• Keywords: EPEW 2008, Input Pepa Model, Internet Technology, Pepa Model, PEPA Stochastic Process