Implementing a Model Checker for Perfomability Behaviour

Holger Hermanns; Joost-Pieter Katoen; Joachim Meyer-Kayser; Markus Siegle

Implementing a Model Checker for Perfomability Behaviour

Holger Hermanns, Joost-Pieter Katoen, Joachim Meyer-Kayser, Markus Siegle

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution › Academic › peer-review

10 Downloads (Pure)

Abstract

We describe a novel model checking algorithm for analysing the behaviour of stochastic systems with respect to their performability. Systems are modelled as actionlabelled CTMCs, and the properties to be veri#ed are speci#ed with the help of the action-based temporal logic aCSL.

Original language	English
Title of host publication	Proceedings of the Fifth International Workshop on Performability Modelling of Computer and Communication Systems (PMCCS 5)
Editors	R. German, J. Lüthi, M. Telek
Place of Publication	Erlangen
Publisher	University of Erlangen
Number of pages	5
Publication status	Published - 2001
Event	5th International Workshop on Performability Modeling of Computer and Communication Systems, PMCCS 2001 - Erlangen, Germany Duration: 15 Sept 2001 → 16 Sept 2001 Conference number: 5

Workshop

Workshop	5th International Workshop on Performability Modeling of Computer and Communication Systems, PMCCS 2001
Abbreviated title	PMCCS
Country/Territory	Germany
City	Erlangen
Period	15/09/01 → 16/09/01

Keywords

METIS-204450

Access to Document

Hermanns2001implementingFinal published version, 220 KB

Cite this

@inproceedings{0f2205dc259b47dc8d48988790a40bd2,

title = "Implementing a Model Checker for Perfomability Behaviour",

abstract = "We describe a novel model checking algorithm for analysing the behaviour of stochastic systems with respect to their performability. Systems are modelled as actionlabelled CTMCs, and the properties to be veri#ed are speci#ed with the help of the action-based temporal logic aCSL.",

keywords = "METIS-204450",

author = "Holger Hermanns and Joost-Pieter Katoen and Joachim Meyer-Kayser and Markus Siegle",

year = "2001",

language = "English",

editor = "R. German and J. L{\"u}thi and M. Telek",

booktitle = "Proceedings of the Fifth International Workshop on Performability Modelling of Computer and Communication Systems (PMCCS 5)",

publisher = "University of Erlangen",

note = "5th International Workshop on Performability Modeling of Computer and Communication Systems, PMCCS 2001, PMCCS ; Conference date: 15-09-2001 Through 16-09-2001",

}

Hermanns, H, Katoen, J-P, Meyer-Kayser, J & Siegle, M 2001, Implementing a Model Checker for Perfomability Behaviour. in R German, J Lüthi & M Telek (eds), Proceedings of the Fifth International Workshop on Performability Modelling of Computer and Communication Systems (PMCCS 5). University of Erlangen, Erlangen, 5th International Workshop on Performability Modeling of Computer and Communication Systems, PMCCS 2001, Erlangen, Germany, 15/09/01.

Implementing a Model Checker for Perfomability Behaviour. / Hermanns, Holger; Katoen, Joost-Pieter; Meyer-Kayser, Joachim et al.
Proceedings of the Fifth International Workshop on Performability Modelling of Computer and Communication Systems (PMCCS 5). ed. / R. German; J. Lüthi; M. Telek. Erlangen: University of Erlangen, 2001.

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution › Academic › peer-review

TY - GEN

T1 - Implementing a Model Checker for Perfomability Behaviour

AU - Hermanns, Holger

AU - Katoen, Joost-Pieter

AU - Meyer-Kayser, Joachim

AU - Siegle, Markus

N1 - Conference code: 5

PY - 2001

Y1 - 2001

N2 - We describe a novel model checking algorithm for analysing the behaviour of stochastic systems with respect to their performability. Systems are modelled as actionlabelled CTMCs, and the properties to be veri#ed are speci#ed with the help of the action-based temporal logic aCSL.

AB - We describe a novel model checking algorithm for analysing the behaviour of stochastic systems with respect to their performability. Systems are modelled as actionlabelled CTMCs, and the properties to be veri#ed are speci#ed with the help of the action-based temporal logic aCSL.

KW - METIS-204450

M3 - Conference contribution

BT - Proceedings of the Fifth International Workshop on Performability Modelling of Computer and Communication Systems (PMCCS 5)

A2 - German, R.

A2 - Lüthi, J.

A2 - Telek, M.

PB - University of Erlangen

CY - Erlangen

T2 - 5th International Workshop on Performability Modeling of Computer and Communication Systems, PMCCS 2001

Y2 - 15 September 2001 through 16 September 2001

ER -