A model checker for performance and dependability properties

H. Hermanns; F. Karelse; Joost P. Katoen; J. Meyer-Kayser; M. Siegle

A model checker for performance and dependability properties

H. Hermanns
, F. Karelse (Editor)
, Joost P. Katoen
, J. Meyer-Kayser
, M. Siegle

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

65 Downloads (Pure)

Abstract

Markov chains are widely used in the context of performance and reliability evaluation of systems of various nature. Model checking of such chains with respect to a given (branching) temporal logic formula has been proposed for both the discrete [8] and the continuous time setting [1], [3]. In this short paper, we describe the prototype model checker $E \vdash M C^2$ for discrete and continuous-time Markov chains, where properties are expressed in appropriate extensions of CTL.We illustrate the general benefits of this approach and discuss the structure of the tool.

Original language	English
Title of host publication	Proceedings of the 2nd PROGRESS Workshop on Embedded Systems 2001
Place of Publication	Veldhoven, the Netherlands
Publisher	STW
Pages	83-88
Number of pages	6
ISBN (Print)	90-73461-27-X
Publication status	Published - 2001
Event	2nd PROGRESS Workshop on Embedded Systems 2001 - Veldhoven, Netherlands Duration: 18 Oct 2001 → 18 Oct 2001 Conference number: 2

Workshop

Workshop	2nd PROGRESS Workshop on Embedded Systems 2001
Abbreviated title	PROGRESS
Country/Territory	Netherlands
City	Veldhoven
Period	18/10/01 → 18/10/01

Keywords

FMT-PM: PROBABILISTIC METHODS
FMT-FMPA: FORMAL METHODS FOR PERFORMANCE ANALYSIS
FMT-MC: MODEL CHECKING
FMT-TOOLS
FMT-RT: VERIFICATION OF REAL-TIME SYSTEMS

Access to Document

Hermanns2001modelFinal published version, 257 KB

Cite this

@inproceedings{d681dfa739ba43acbf3b502d6c0de182,

title = "A model checker for performance and dependability properties",

abstract = "Markov chains are widely used in the context of performance and reliability evaluation of systems of various nature. Model checking of such chains with respect to a given (branching) temporal logic formula has been proposed for both the discrete [8] and the continuous time setting [1], [3]. In this short paper, we describe the prototype model checker \$E \textbackslash{}vdash M C\textasciicircum{}2\$ for discrete and continuous-time Markov chains, where properties are expressed in appropriate extensions of CTL.We illustrate the general benefits of this approach and discuss the structure of the tool.",

keywords = "FMT-PM: PROBABILISTIC METHODS, FMT-FMPA: FORMAL METHODS FOR PERFORMANCE ANALYSIS, FMT-MC: MODEL CHECKING, FMT-TOOLS, FMT-RT: VERIFICATION OF REAL-TIME SYSTEMS",

author = "H. Hermanns and F. Karelse and Katoen, \{Joost P.\} and J. Meyer-Kayser and M. Siegle",

year = "2001",

language = "English",

isbn = "90-73461-27-X",

pages = "83--88",

booktitle = "Proceedings of the 2nd PROGRESS Workshop on Embedded Systems 2001",

publisher = "STW",

note = "2nd PROGRESS Workshop on Embedded Systems 2001, PROGRESS ; Conference date: 18-10-2001 Through 18-10-2001",

}

TY - GEN

T1 - A model checker for performance and dependability properties

AU - Hermanns, H.

AU - Katoen, Joost P.

AU - Meyer-Kayser, J.

AU - Siegle, M.

A2 - Karelse, F.

N1 - Conference code: 2

PY - 2001

Y1 - 2001

N2 - Markov chains are widely used in the context of performance and reliability evaluation of systems of various nature. Model checking of such chains with respect to a given (branching) temporal logic formula has been proposed for both the discrete [8] and the continuous time setting [1], [3]. In this short paper, we describe the prototype model checker $E \vdash M C^2$ for discrete and continuous-time Markov chains, where properties are expressed in appropriate extensions of CTL.We illustrate the general benefits of this approach and discuss the structure of the tool.

AB - Markov chains are widely used in the context of performance and reliability evaluation of systems of various nature. Model checking of such chains with respect to a given (branching) temporal logic formula has been proposed for both the discrete [8] and the continuous time setting [1], [3]. In this short paper, we describe the prototype model checker $E \vdash M C^2$ for discrete and continuous-time Markov chains, where properties are expressed in appropriate extensions of CTL.We illustrate the general benefits of this approach and discuss the structure of the tool.

KW - FMT-PM: PROBABILISTIC METHODS

KW - FMT-FMPA: FORMAL METHODS FOR PERFORMANCE ANALYSIS

KW - FMT-MC: MODEL CHECKING

KW - FMT-TOOLS

KW - FMT-RT: VERIFICATION OF REAL-TIME SYSTEMS

M3 - Conference contribution

SN - 90-73461-27-X

SP - 83

EP - 88

BT - Proceedings of the 2nd PROGRESS Workshop on Embedded Systems 2001

PB - STW

CY - Veldhoven, the Netherlands

T2 - 2nd PROGRESS Workshop on Embedded Systems 2001

Y2 - 18 October 2001 through 18 October 2001

ER -

A model checker for performance and dependability properties

Abstract

Workshop

Keywords

Access to Document

Fingerprint

Cite this