author = {Tamas Berczes and Gabor Guta and Gabor Kusper and Wolfgang Schreiner and Janos Sztrik},
title = {{Evaluating a Probabilistic Model Checker for Modeling and Analyzing Retrial Queueing Systems }},
language = {english},
abstract = {We describe the results of analyzing the performance model of a retrial queueing system with the PRISM (PRobabIlistic Symbolic Model checker). The system has been previously analyzed with the help of the performance modeling environment MOSEL (Modeling, Specification and Evaluation Language). In our paper we are able to accurately reproduce the results reported in literature. Furthermore, we compare PRISM and MOSEL with respect to their modeling languages and ways of specifying performance queries and benchmark the executions of the tools. Several numerical examples illustrate the comparisons resulting in various tables and figures.},
journal = {Annales Mathematicae et Informaticae},
pages = {--},
publisher = {Liceum University Press},
isbn_issn = {ISSN 1787-5021},
year = {2010},
month = {December},
refereed = {yes},
keywords = {retrial queueing systems, probablisitic model checking, MOSEL, PRISM},
sponsor = {Supported by the Austrian-Hungarian Scientific/Technical Cooperation Contract HU 13/2007 and Hungarian Scientific Research Fund- OTKA K 60698/2006},
length = {30},
url = {http://ami.ektf.hu/}