Model-checking performability properties

Boudewijn Haverkort; Lucia Cloth; Holger Hermanns; Joost P. Katoen; Christel Baier

doi:10.1109/DSN.2002.1028891

Model-checking performability properties

Boudewijn Haverkort, Lucia Cloth, Holger Hermanns, Joost P. Katoen, Christel Baier

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

62 Citations (Scopus)

25 Downloads (Pure)

Abstract

Model checking has been introduced as an automated technique to verify whether functional properties, expressed in a formal logic like computational tree logic (CTL), do hold in a formally-specified system. We present a number of computational procedures to perform model checking of continuous stochastic reward logic (CSRL) over finite Markov reward models, thereby stressing their computational complexity (time and space) and applicability from a practical point of view (accuracy, stability). A case study in the area of ad hoc mobile computing under power constraints shows the merits of CSRL and the new computational procedures.

Original language	English
Title of host publication	Proceedings International Conference on Dependable Systems and Networks (DSN)
Subtitle of host publication	23-26 June 2002, Washington, D.C., USA
Publisher	IEEE
Pages	103-112
Number of pages	10
ISBN (Electronic)	0-7695-1599-1
ISBN (Print)	0-7695-1597-5, 0-7695-1598-3
DOIs	https://doi.org/10.1109/DSN.2002.1028891
Publication status	Published - 2002
Event	International Conference on Dependable Systems and Networks, DSN 2002 - Washington, United States Duration: 23 Jun 2002 → 26 Jun 2002

Other

Other	International Conference on Dependable Systems and Networks, DSN 2002
Abbreviated title	DSN
Country/Territory	United States
City	Washington
Period	23/06/02 → 26/06/02

Keywords

FMT-PM: PROBABILISTIC METHODS
FMT-MC: MODEL CHECKING
FMT-FMPA: FORMAL METHODS FOR PERFORMANCE ANALYSIS

Access to Document

10.1109/DSN.2002.1028891

Cite this

@inproceedings{53ec0ddd2d6f4d61ac792157019937f6,

title = "Model-checking performability properties",

abstract = "Model checking has been introduced as an automated technique to verify whether functional properties, expressed in a formal logic like computational tree logic (CTL), do hold in a formally-specified system. We present a number of computational procedures to perform model checking of continuous stochastic reward logic (CSRL) over finite Markov reward models, thereby stressing their computational complexity (time and space) and applicability from a practical point of view (accuracy, stability). A case study in the area of ad hoc mobile computing under power constraints shows the merits of CSRL and the new computational procedures.",

keywords = "FMT-PM: PROBABILISTIC METHODS, FMT-MC: MODEL CHECKING, FMT-FMPA: FORMAL METHODS FOR PERFORMANCE ANALYSIS",

author = "Boudewijn Haverkort and Lucia Cloth and Holger Hermanns and Katoen, {Joost P.} and Christel Baier",

year = "2002",

doi = "10.1109/DSN.2002.1028891",

language = "English",

isbn = "0-7695-1597-5",

pages = "103--112",

booktitle = "Proceedings International Conference on Dependable Systems and Networks (DSN)",

publisher = "IEEE",

address = "United States",

note = "International Conference on Dependable Systems and Networks, DSN 2002, DSN ; Conference date: 23-06-2002 Through 26-06-2002",

}

Haverkort, B, Cloth, L, Hermanns, H, Katoen, JP & Baier, C 2002, Model-checking performability properties. in Proceedings International Conference on Dependable Systems and Networks (DSN): 23-26 June 2002, Washington, D.C., USA. IEEE, pp. 103-112, International Conference on Dependable Systems and Networks, DSN 2002, Washington, District of Columbia, United States, 23/06/02. https://doi.org/10.1109/DSN.2002.1028891

TY - GEN

T1 - Model-checking performability properties

AU - Haverkort, Boudewijn

AU - Cloth, Lucia

AU - Hermanns, Holger

AU - Katoen, Joost P.

AU - Baier, Christel

PY - 2002

Y1 - 2002

N2 - Model checking has been introduced as an automated technique to verify whether functional properties, expressed in a formal logic like computational tree logic (CTL), do hold in a formally-specified system. We present a number of computational procedures to perform model checking of continuous stochastic reward logic (CSRL) over finite Markov reward models, thereby stressing their computational complexity (time and space) and applicability from a practical point of view (accuracy, stability). A case study in the area of ad hoc mobile computing under power constraints shows the merits of CSRL and the new computational procedures.

AB - Model checking has been introduced as an automated technique to verify whether functional properties, expressed in a formal logic like computational tree logic (CTL), do hold in a formally-specified system. We present a number of computational procedures to perform model checking of continuous stochastic reward logic (CSRL) over finite Markov reward models, thereby stressing their computational complexity (time and space) and applicability from a practical point of view (accuracy, stability). A case study in the area of ad hoc mobile computing under power constraints shows the merits of CSRL and the new computational procedures.

KW - FMT-PM: PROBABILISTIC METHODS

KW - FMT-MC: MODEL CHECKING

KW - FMT-FMPA: FORMAL METHODS FOR PERFORMANCE ANALYSIS

U2 - 10.1109/DSN.2002.1028891

DO - 10.1109/DSN.2002.1028891

M3 - Conference contribution

SN - 0-7695-1597-5

SN - 0-7695-1598-3

SP - 103

EP - 112

BT - Proceedings International Conference on Dependable Systems and Networks (DSN)

PB - IEEE

T2 - International Conference on Dependable Systems and Networks, DSN 2002

Y2 - 23 June 2002 through 26 June 2002

ER -

Model-checking performability properties

Abstract

Other

Keywords

Access to Document

Fingerprint

Cite this