Implementing a Model Checker for Perfomability Behaviour

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

Research output: Chapter in Book/Report/Conference proceedingConference contributionAcademicpeer-review

1 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 languageEnglish
Title of host publicationProceedings of the Fifth International Workshop on Performability Modelling of Computer and Communication Systems (PMCCS 5)
EditorsR. German, J. Lüthi, M. Telek
Place of PublicationErlangen
PublisherUniversity of Erlangen
Number of pages5
Publication statusPublished - 2001
Event5th International Workshop on Performability Modeling of Computer and Communication Systems, PMCCS 2001 - Erlangen, Germany
Duration: 15 Sep 200116 Sep 2001
Conference number: 5

Workshop

Workshop5th International Workshop on Performability Modeling of Computer and Communication Systems, PMCCS 2001
Abbreviated titlePMCCS
CountryGermany
CityErlangen
Period15/09/0116/09/01

Fingerprint

Performability
Temporal Logic
Stochastic Systems
Model Checking
Model

Keywords

  • METIS-204450

Cite this

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) Erlangen: University of Erlangen.
Hermanns, Holger ; Katoen, Joost-Pieter ; Meyer-Kayser, Joachim ; Siegle, Markus. / Implementing a Model Checker for Perfomability Behaviour. Proceedings of the Fifth International Workshop on Performability Modelling of Computer and Communication Systems (PMCCS 5). editor / R. German ; J. Lüthi ; M. Telek. Erlangen : University of Erlangen, 2001.
@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",

}

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; Siegle, Markus.

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 proceedingConference contributionAcademicpeer-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

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

ER -

Hermanns H, Katoen J-P, Meyer-Kayser J, Siegle M. Implementing a Model Checker for Perfomability Behaviour. In German R, Lüthi J, Telek M, editors, Proceedings of the Fifth International Workshop on Performability Modelling of Computer and Communication Systems (PMCCS 5). Erlangen: University of Erlangen. 2001