Abstraction and Model Checking in the PEPA Plug-In for Eclipse

The stochastic process algebra PEPA is widely used for performance modelling, and a large part of its success is due to its rich tool support. As a compositional Markovian formalism, however, it suffers from the state space explosion problem, where even small models can lead to very large Markov chains. One way of analysing such models is to use abstraction - constructing a smaller model that bounds the properties of the original. We present an extension to the PEPA plug-in for Eclipse that enables abstracting and model checking of PEPA models. This implements two new features. The abstraction view provides a graphical interface for labelling and aggregating states of individual PEPA components. The model checking view provides an interface for constructing CSL properties, which are then verified with respect to the specified abstraction. We have an internal CSL model checker for CTMDPs, so the tool can be used as a stand-alone.