Model-checking performability properties

Boudewijn R.H.M. Haverkort, L. Cloth, H. Hermanns, Joost P. Katoen, Christel Baier

Research output: Contribution to conferencePaperAcademicpeer-review

13 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 languageEnglish
Pages103-112
Number of pages10
DOIs
Publication statusPublished - 2002
EventInternational Conference on Dependable Systems and Networks, DSN 2002 - Washington, United States
Duration: 23 Jun 200226 Jun 2002

Other

OtherInternational Conference on Dependable Systems and Networks, DSN 2002
Abbreviated titleDSN
CountryUnited States
CityWashington
Period23/06/0226/06/02

Fingerprint

Model checking
Formal logic
Mobile computing
Computational complexity

Keywords

  • FMT-PM: PROBABILISTIC METHODS
  • FMT-MC: MODEL CHECKING
  • IR-63324
  • FMT-FMPA: FORMAL METHODS FOR PERFORMANCE ANALYSIS
  • EWI-6523

Cite this

Haverkort, B. R. H. M., Cloth, L., Hermanns, H., Katoen, J. P., & Baier, C. (2002). Model-checking performability properties. 103-112. Paper presented at International Conference on Dependable Systems and Networks, DSN 2002, Washington, United States. https://doi.org/10.1109/DSN.2002.1028891
Haverkort, Boudewijn R.H.M. ; Cloth, L. ; Hermanns, H. ; Katoen, Joost P. ; Baier, Christel. / Model-checking performability properties. Paper presented at International Conference on Dependable Systems and Networks, DSN 2002, Washington, United States.10 p.
@conference{c4988172c82f4555880f08aa4448b70b,
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, IR-63324, FMT-FMPA: FORMAL METHODS FOR PERFORMANCE ANALYSIS, EWI-6523",
author = "Haverkort, {Boudewijn R.H.M.} and L. Cloth and H. Hermanns and Katoen, {Joost P.} and Christel Baier",
year = "2002",
doi = "10.1109/DSN.2002.1028891",
language = "English",
pages = "103--112",
note = "International Conference on Dependable Systems and Networks, DSN 2002, DSN ; Conference date: 23-06-2002 Through 26-06-2002",

}

Haverkort, BRHM, Cloth, L, Hermanns, H, Katoen, JP & Baier, C 2002, 'Model-checking performability properties' Paper presented at International Conference on Dependable Systems and Networks, DSN 2002, Washington, United States, 23/06/02 - 26/06/02, pp. 103-112. https://doi.org/10.1109/DSN.2002.1028891

Model-checking performability properties. / Haverkort, Boudewijn R.H.M.; Cloth, L.; Hermanns, H.; Katoen, Joost P.; Baier, Christel.

2002. 103-112 Paper presented at International Conference on Dependable Systems and Networks, DSN 2002, Washington, United States.

Research output: Contribution to conferencePaperAcademicpeer-review

TY - CONF

T1 - Model-checking performability properties

AU - Haverkort, Boudewijn R.H.M.

AU - Cloth, L.

AU - Hermanns, H.

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 - IR-63324

KW - FMT-FMPA: FORMAL METHODS FOR PERFORMANCE ANALYSIS

KW - EWI-6523

U2 - 10.1109/DSN.2002.1028891

DO - 10.1109/DSN.2002.1028891

M3 - Paper

SP - 103

EP - 112

ER -

Haverkort BRHM, Cloth L, Hermanns H, Katoen JP, Baier C. Model-checking performability properties. 2002. Paper presented at International Conference on Dependable Systems and Networks, DSN 2002, Washington, United States. https://doi.org/10.1109/DSN.2002.1028891