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

Michael James Andrew Smith

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

Michael James Andrew Smith

Research output: Chapter in Book/Report/Conference proceeding › Article in proceedings › Research › peer-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 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, VA, United States Duration: 15 Sep 2010 → 18 Sep 2010 Conference number: 7 http://www.qest.org/qest2010/

Conference

Conference	7th International Conference on Quantitative Evaluation of Systems
Number	7
Country	United States
City	Williamsburg, VA
Period	15/09/2010 → 18/09/2010
Internet address	http://www.qest.org/qest2010/

Access to Document

http://www.qest.org/qest2010/

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

@inproceedings{266d98a3d5a74ef2bbe0b9ba6162c7f6,

title = "Abstraction and Model Checking in the PEPA Plug-in for Eclipse",

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.",

author = "Smith, {Michael James Andrew}",

year = "2010",

language = "English",

pages = "155--156",

booktitle = "Proceedings of the 7th International Conference on Quantitative Evaluation of Systems (QEST 2010)",

publisher = "IEEE Computer Society Press",

note = "7th International Conference on Quantitative Evaluation of Systems, QEST'10 ; Conference date: 15-09-2010 Through 18-09-2010",

url = "http://www.qest.org/qest2010/",

}

TY - GEN

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

AU - Smith, Michael James Andrew

N1 - Conference code: 7

PY - 2010

Y1 - 2010

N2 - 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.

AB - 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.

M3 - Article in proceedings

SP - 155

EP - 156

BT - Proceedings of the 7th International Conference on Quantitative Evaluation of Systems (QEST 2010)

PB - IEEE Computer Society Press

T2 - 7th International Conference on Quantitative Evaluation of Systems

Y2 - 15 September 2010 through 18 September 2010

ER -