author = {Wolfgang Schreiner and János Sztrik},
title = {{Applying Statistical Model Checking to the Analysis of a Retrial Queueing System with Constant Time Impatience}},
language = {english},
abstract = {We report on experiments with the automated analysis of a finite-source queueing system with an unreliable server where clients abort unserved requests after some maximum (con- stant) amount of time. In earlier work, we created a CTMC model of this system where the constant time bound was approximated by an Erlang distribution and analyzed this model with the probabilistic model checker PRISM. However, due to state space explosion only instances of the system with a very small number of clients could be analyzed. In this paper, we extend the results to larger systems by applying the statistical model checking capabilities of PRISM where results are approximated by sampling a large number of simulation runs. In particular, we address the change from the analysis of the steady state behavior of the system to the analysis of finite runs of the system and the trade-off between the accuracy of the results and the computational efforts needed to derive them.},
number = {19-12},
year = {2019},
month = {September},
keywords = {performance modeling, formal methods, probabilistic model checking},
sponsor = {Supported by the Aktion Österreich-Ungarn project 101öu7.},
length = {11},
type = {RISC Report Series},
institution = {Research Institute for Symbolic Computation (RISC), Johannes Kepler University Linz},
address = {Altenberger Straße 69, 4040 Linz, Austria},
issn = {2791-4267 (online)}