Performance Analysis of Real-time Systems and Software Designs [HU 10/2012]

Project Lead

Project Duration

01/12/2012 - 30/11/2014

Project URL

Project Website



Probabilistic Model Checking on HPC Systems for the Performance Analysis of Mobile Networks

Wolfgang Schreiner, Tamas Berczes, Janos Sztrik

Annales Mathematicae et Informaticae 43, pp. 123-144. 2014. Líceum University Press, ISSN 1787-5021, ISSN 1787-6117.
author = {Wolfgang Schreiner and Tamas Berczes and Janos Sztrik},
title = {{Probabilistic Model Checking on HPC Systems for the Performance Analysis of Mobile Networks}},
language = {english},
abstract = {We report on the use of HPC resources for the performance analysis of the mobilecellular network model described in “A New Finite-Source Queueing Model forMobile Cellular Networks Applying Spectrum Renting” by Tien Van Do et al. Thatpaper proposed a new finite-source retrial queueing model with spectrum renting thatwas analyzed with the MOSEL-2 tool. Our results show how this model can be alsoappropriately described and analyzed with the probabilistic model checker PRISM, althoughat some cost considering the formulation of the model; in particular, we are ableto accurately reproduce most of the analytical results presented in that paper and thusincrease the confidence in the previously presented results. However, we also outlinesome discrepancies which may hint to deficiencies of the original analysis. Moreover,by applying a parallel computing framework developed for this purpose, we are ableto considerably speed up studies performed with the PRISM tool. The investigationsare illustrated by figures and conclusions are drawn.},
journal = {Annales Mathematicae et Informaticae},
volume = {43},
pages = {123--144},
publisher = {Líceum University Press},
isbn_issn = {ISSN 1787-5021, ISSN 1787-6117},
year = {2014},
refereed = {yes},
length = {22}