Derivation of Passage-time Densities in PEPA Models using ipc: the Imperial PEPA Compiler

We present a technique for defining and extracting passage-time densities from high-level stochastic process algebra models. Our high-level formalism is PEPA, a popular Markovian process algebra for expressing compositional performance models. We introduce ipc, a tool which can process PEPA-specified passage-time densities and models by compiling the PEPA model and passage specification into the DNAmaca formalism. DNAmaca is an established modelling language for the low-level specification of very large Markov and semi-Markov chains. We provide performance results for ipc/DNAmaca and comparisons with another tool which supports PEPA, PRISM. Finally, we generate passage-time densities and quantiles for a case study of a high-availability web server.

• Type: Conference
• Year: 2003
• Where: MASCOTS
• Authors: Jeremy T. Bradley, Nicholas J. Dingle, Stephen T. Gilmore, William J. Knottenbelt
• Keywords: MASCOTS 2003, MASCOTS 2007, Passage-time Densities, Process Algebra, Process Algebra Models