The PEPA Plug-in Project
The PEPA Plug-in Project is a software tool that supports the stochastic process algebra PEPA.
PEPA is a formal language which allows quantitative analysis of systems. Models can be described in a compositional way - as cooperation between individual automata that carry out actions. By associating rates to each action of the model, the description is interpreted against an interleaving semantics which gives rise to an underlying Continuous Time Markov Chain. Typical questions that can be answered by the analysis of the Markov chain are the throughput of an action or the utilisation of a component.
More recently, a fluid approximation has been proposed to cope with state space explosion. This leads to an underlying mathematical representation in the form of a system of Ordinary Differential Equations, which scale very well with large state spaces.
For more information about PEPA, visit the PEPA web site at http://www.dcs.ed.ac.uk/pepa/.
The tool enables Markovian steady-state as well as ODE analysis of PEPA models, and now has a new interface for abstracting and model checking Continuous Stochastic Logic (CSL) properties. It is deployed as a contribution to the Eclipse framework. If you are new to Eclipse, visit the Eclipse web site. In short, that means that you must have the Eclipse IDE installed to install the PEPA Plug-in Project.
In addition to a user-friendly graphical interface, it also provides an easy-to-use API that exposes the core tool library PEPAto to third-party Eclipse plug-ins.
For more information on how to install the tool, visit the Download section.
Development of the abstraction and model checking features of the tool was supported by a Microsoft Research European Scholarship.