Computing Response Time Distributions Using Iterative Probabilistic Model Checking

Freek van den Berg, Jozef Hooman, Arnd Hartmanns, Boudewijn R.H.M. Haverkort, Anne Katharina Ingrid Remke

Research output: Chapter in Book/Report/Conference proceedingConference contribution

  • 8 Citations

Abstract

System designers need to have insight in the response times of service systems to see if they meet performance requirements. We present a high-level evaluation technique to obtain the distribution of services completion times. It is based on a high-level domain-specific language that hides the underlying technicalities from the system designer. Under the hood, probabilistic real-time model checking technology is used iteratively to obtain precise bounds and probabilities. This allows reasoning about nondeterministic, probabilistic and real-time aspects in a single evaluation. To reduce the state spaces for analysis, we use two sampling methods (for measurements) that simplify the system model: (i) applying an abstraction on time by increasing the length of a (discrete) model time unit, and (ii) computing only absolute bounds by replacing probabilistic choices with non-deterministic ones. We use an industrial case on image processing of an interventional X-ray system to illustrate our approach.
LanguageUndefined
Title of host publicationProceedings of the 12th European Workshop on Computer Performance Engineering, EPEW 2015
EditorsMarta Beltran, William Knottenbelt, Jeremy Bradley
Place of PublicationBerlin
PublisherSpringer
Pages208-224
Number of pages17
ISBN (Print)978-3-319-23266-9
DOIs
StatePublished - 31 Aug 2015

Publication series

NameLecture notes in computer science
PublisherSpringer Verlag
Volume9272
ISSN (Print)0302-9743
ISSN (Electronic)1611-3349

Keywords

  • EWI-26291
  • IR-98151
  • METIS-314965

Cite this

van den Berg, F., Hooman, J., Hartmanns, A., Haverkort, B. R. H. M., & Remke, A. K. I. (2015). Computing Response Time Distributions Using Iterative Probabilistic Model Checking. In M. Beltran, W. Knottenbelt, & J. Bradley (Eds.), Proceedings of the 12th European Workshop on Computer Performance Engineering, EPEW 2015 (pp. 208-224). (Lecture notes in computer science; Vol. 9272). Berlin: Springer. DOI: 10.1007/978-3-319-23267-6_14
van den Berg, Freek ; Hooman, Jozef ; Hartmanns, Arnd ; Haverkort, Boudewijn R.H.M. ; Remke, Anne Katharina Ingrid. / Computing Response Time Distributions Using Iterative Probabilistic Model Checking. Proceedings of the 12th European Workshop on Computer Performance Engineering, EPEW 2015. editor / Marta Beltran ; William Knottenbelt ; Jeremy Bradley. Berlin : Springer, 2015. pp. 208-224 (Lecture notes in computer science).
@inproceedings{789afa556c5341298c13cd2ad630cc8a,
title = "Computing Response Time Distributions Using Iterative Probabilistic Model Checking",
abstract = "System designers need to have insight in the response times of service systems to see if they meet performance requirements. We present a high-level evaluation technique to obtain the distribution of services completion times. It is based on a high-level domain-specific language that hides the underlying technicalities from the system designer. Under the hood, probabilistic real-time model checking technology is used iteratively to obtain precise bounds and probabilities. This allows reasoning about nondeterministic, probabilistic and real-time aspects in a single evaluation. To reduce the state spaces for analysis, we use two sampling methods (for measurements) that simplify the system model: (i) applying an abstraction on time by increasing the length of a (discrete) model time unit, and (ii) computing only absolute bounds by replacing probabilistic choices with non-deterministic ones. We use an industrial case on image processing of an interventional X-ray system to illustrate our approach.",
keywords = "EWI-26291, IR-98151, METIS-314965",
author = "{van den Berg}, Freek and Jozef Hooman and Arnd Hartmanns and Haverkort, {Boudewijn R.H.M.} and Remke, {Anne Katharina Ingrid}",
note = "eemcs-eprint-26291",
year = "2015",
month = "8",
day = "31",
doi = "10.1007/978-3-319-23267-6_14",
language = "Undefined",
isbn = "978-3-319-23266-9",
series = "Lecture notes in computer science",
publisher = "Springer",
pages = "208--224",
editor = "Marta Beltran and William Knottenbelt and Jeremy Bradley",
booktitle = "Proceedings of the 12th European Workshop on Computer Performance Engineering, EPEW 2015",

}

van den Berg, F, Hooman, J, Hartmanns, A, Haverkort, BRHM & Remke, AKI 2015, Computing Response Time Distributions Using Iterative Probabilistic Model Checking. in M Beltran, W Knottenbelt & J Bradley (eds), Proceedings of the 12th European Workshop on Computer Performance Engineering, EPEW 2015. Lecture notes in computer science, vol. 9272, Springer, Berlin, pp. 208-224. DOI: 10.1007/978-3-319-23267-6_14

Computing Response Time Distributions Using Iterative Probabilistic Model Checking. / van den Berg, Freek; Hooman, Jozef; Hartmanns, Arnd; Haverkort, Boudewijn R.H.M.; Remke, Anne Katharina Ingrid.

Proceedings of the 12th European Workshop on Computer Performance Engineering, EPEW 2015. ed. / Marta Beltran; William Knottenbelt; Jeremy Bradley. Berlin : Springer, 2015. p. 208-224 (Lecture notes in computer science; Vol. 9272).

Research output: Chapter in Book/Report/Conference proceedingConference contribution

TY - GEN

T1 - Computing Response Time Distributions Using Iterative Probabilistic Model Checking

AU - van den Berg,Freek

AU - Hooman,Jozef

AU - Hartmanns,Arnd

AU - Haverkort,Boudewijn R.H.M.

AU - Remke,Anne Katharina Ingrid

N1 - eemcs-eprint-26291

PY - 2015/8/31

Y1 - 2015/8/31

N2 - System designers need to have insight in the response times of service systems to see if they meet performance requirements. We present a high-level evaluation technique to obtain the distribution of services completion times. It is based on a high-level domain-specific language that hides the underlying technicalities from the system designer. Under the hood, probabilistic real-time model checking technology is used iteratively to obtain precise bounds and probabilities. This allows reasoning about nondeterministic, probabilistic and real-time aspects in a single evaluation. To reduce the state spaces for analysis, we use two sampling methods (for measurements) that simplify the system model: (i) applying an abstraction on time by increasing the length of a (discrete) model time unit, and (ii) computing only absolute bounds by replacing probabilistic choices with non-deterministic ones. We use an industrial case on image processing of an interventional X-ray system to illustrate our approach.

AB - System designers need to have insight in the response times of service systems to see if they meet performance requirements. We present a high-level evaluation technique to obtain the distribution of services completion times. It is based on a high-level domain-specific language that hides the underlying technicalities from the system designer. Under the hood, probabilistic real-time model checking technology is used iteratively to obtain precise bounds and probabilities. This allows reasoning about nondeterministic, probabilistic and real-time aspects in a single evaluation. To reduce the state spaces for analysis, we use two sampling methods (for measurements) that simplify the system model: (i) applying an abstraction on time by increasing the length of a (discrete) model time unit, and (ii) computing only absolute bounds by replacing probabilistic choices with non-deterministic ones. We use an industrial case on image processing of an interventional X-ray system to illustrate our approach.

KW - EWI-26291

KW - IR-98151

KW - METIS-314965

U2 - 10.1007/978-3-319-23267-6_14

DO - 10.1007/978-3-319-23267-6_14

M3 - Conference contribution

SN - 978-3-319-23266-9

T3 - Lecture notes in computer science

SP - 208

EP - 224

BT - Proceedings of the 12th European Workshop on Computer Performance Engineering, EPEW 2015

PB - Springer

CY - Berlin

ER -

van den Berg F, Hooman J, Hartmanns A, Haverkort BRHM, Remke AKI. Computing Response Time Distributions Using Iterative Probabilistic Model Checking. In Beltran M, Knottenbelt W, Bradley J, editors, Proceedings of the 12th European Workshop on Computer Performance Engineering, EPEW 2015. Berlin: Springer. 2015. p. 208-224. (Lecture notes in computer science). Available from, DOI: 10.1007/978-3-319-23267-6_14