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

Michael James Andrew Smith

    Research output: Chapter in Book/Report/Conference proceedingArticle in proceedingsResearchpeer-review

    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 languageEnglish
    Title of host publicationProceedings of the 7th International Conference on Quantitative Evaluation of Systems (QEST 2010)
    PublisherIEEE Computer Society Press
    Publication date2010
    Pages155-156
    Publication statusPublished - 2010
    Event7th International Conference on Quantitative Evaluation of Systems - Williamsburg, VA, United States
    Duration: 15 Sep 201018 Sep 2010
    Conference number: 7
    http://www.qest.org/qest2010/

    Conference

    Conference7th International Conference on Quantitative Evaluation of Systems
    Number7
    CountryUnited States
    CityWilliamsburg, VA
    Period15/09/201018/09/2010
    Internet address

    Fingerprint Dive into the research topics of 'Abstraction and Model Checking in the PEPA Plug-in for Eclipse'. Together they form a unique fingerprint.

    Cite this