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.
Gabriele Kotsis (Ed.)
pubs.doc.ic.ac.uk: built & maintained by Ashok Argent-Katwala.