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.
|Title of host publication||Proceedings of the 12th European Workshop on Computer Performance Engineering (EPEW 2015)|
|Editors||Marta Beltran, William Knottenbelt, Jeremy Bradley|
|Place of Publication||Cham|
|Number of pages||17|
|Publication status||Published - 31 Aug 2015|
|Name||Lecture notes in computer science|
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). Cham: Springer. https://doi.org/10.1007/978-3-319-23267-6_14