Abstract
The stochastic process algebra PEPA is a widely used language for performance modelling, and a large part of its success is due to the rich tool support that is available. 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.
Original language | English |
---|---|
Title of host publication | Proceedings of the 7th International Conference on Quantitative Evaluation of Systems (QEST 2010) |
Publisher | IEEE Computer Society Press |
Publication date | 2010 |
Pages | 155-156 |
Publication status | Published - 2010 |
Event | 7th International Conference on Quantitative Evaluation of Systems - Williamsburg, United States Duration: 15 Sept 2010 → 18 Sept 2010 Conference number: 7 http://www.qest.org/qest2010/ |
Conference
Conference | 7th International Conference on Quantitative Evaluation of Systems |
---|---|
Number | 7 |
Country/Territory | United States |
City | Williamsburg |
Period | 15/09/2010 → 18/09/2010 |
Internet address |