Computing response time distributions using iterative probabilistic model checking

Van Den Berg, Freek; Hooman, Jozef; Hartmanns, Arnd; Haverkort, Boudewijn R.; Remke, Anne

doi:10.1007/978-3-319-23267-6

Computing response time distributions using iterative probabilistic model checking

Title

Computing response time distributions using iterative probabilistic model checking

Author

Van Den Berg, Freek
Hooman, Jozef
Hartmanns, Arnd
Haverkort, Boudewijn R.
Remke, Anne

Contributor

Beltrán, Marta (editor)
Knottenbelt, William (editor)
Bradley, Jeremy (editor)

Publication year

2015

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.

Subject

ICT
ESI - Embedded Systems Innovation
TS - Technical Sciences
High Tech Systems & Materials
Informatics
Industrial Innovation
Computer programming languages
High level languages
Image processing
Iterative methods
Probability distributions
Problem oriented languages
Response time (computer systems)
Systems analysis
High-level domain
Performance requirements
Probabilistic choices
Probabilistic model checking
Real time aspects
Real time modeling
Response time distribution
System designers