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||Berlin|
|Number of pages||16|
|Publication status||Published - 30 Aug 2015|
|Name||Lecture Notes in Computer Science|