Implementing a Model Checker for Performability Behaviour

H. Hermanns; R. German; Joost P. Katoen; J. Meyer-Kayser

Implementing a Model Checker for Performability Behaviour

H. Hermanns, R. German (Editor), Joost P. Katoen, J. Meyer-Kayser

Research output: Contribution to conference › Paper › peer-review

68 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 verified are specified with the help of the action-based temporal logic aCSL. The technique is currently being implemented in our freely available prototype tool ETMCC.

Original language	Undefined
Pages	110-114
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

FMT-PA: PROCESS ALGEBRAS
FMT-PM: PROBABILISTIC METHODS
IR-66282
EWI-6518
FMT-FMPA: FORMAL METHODS FOR PERFORMANCE ANALYSIS
FMT-TOOLS

Access to Document

Cite this

@conference{8f73beba0c974faf84b000816db0e109,

title = "Implementing a Model Checker for Performability 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 verified are specified with the help of the action-based temporal logic aCSL. The technique is currently being implemented in our freely available prototype tool ETMCC.",

keywords = "FMT-PA: PROCESS ALGEBRAS, FMT-PM: PROBABILISTIC METHODS, IR-66282, EWI-6518, FMT-FMPA: FORMAL METHODS FOR PERFORMANCE ANALYSIS, FMT-TOOLS",

author = "H. Hermanns and R. German and Katoen, {Joost P.} and J. Meyer-Kayser",

year = "2001",

language = "Undefined",

pages = "110--114",

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

}

TY - CONF

T1 - Implementing a Model Checker for Performability Behaviour

AU - Hermanns, H.

AU - Katoen, Joost P.

AU - Meyer-Kayser, J.

A2 - German, R.

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 verified are specified with the help of the action-based temporal logic aCSL. The technique is currently being implemented in our freely available prototype tool ETMCC.

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 verified are specified with the help of the action-based temporal logic aCSL. The technique is currently being implemented in our freely available prototype tool ETMCC.

KW - FMT-PA: PROCESS ALGEBRAS

KW - FMT-PM: PROBABILISTIC METHODS

KW - IR-66282

KW - EWI-6518

KW - FMT-FMPA: FORMAL METHODS FOR PERFORMANCE ANALYSIS

KW - FMT-TOOLS

M3 - Paper

SP - 110

EP - 114

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

Y2 - 15 September 2001 through 16 September 2001

ER -