Applying Statistical Model Checking to the Analysis of a Retrial Queueing System with Constant Time Impatience

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.