Analzying Real-Time Systems by Combining Temporal Logic and Statistical Models

Project Lead

Project Duration

01/01/2007 - 31/12/2008

Project URL

Go to Website

Publications

2010

[Guta]

Evaluating a Probabilistic Model Checker for Modeling and Analyzing Retrial Queueing Systems

Tamas Berczes, Gabor Guta, Gabor Kusper, Wolfgang Schreiner, Janos Sztrik

Annales Mathematicae et Informaticae, pp. -. December 2010. Liceum University Press, ISSN 1787-5021. [url]
[bib]
@article{RISC4029,
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 retrialqueueing system with the PRISM (PRobabIlistic Symbolic Model checker).The system has been previously analyzed with the help of the performance modelingenvironment 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 modelinglanguages and ways of specifying performance queries and benchmark the executionsof the tools. Several numerical examples illustrate the comparisons resultingin 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/}
}

2009

[Guta]

Analyzing a Proxy Cache Server Performance Model with the Probabilistic Model Checker PRISM

Tamás Bérczes, Gábor Guta, Gábor Kusper, Wolfgang Schreiner, János Sztrik

In: WWV'09, 5th Int'l Workshop on Automated Specification and Verification of Web Systems, Demis Ballis, Temur Kutsia (ed.), pp. -. July 2009. Hagenberg, Austria, -. [pdf]
[bib]
@inproceedings{RISC3821,
author = {Tamás Bérczes and Gábor Guta and Gábor Kusper and Wolfgang Schreiner and János Sztrik},
title = {{Analyzing a Proxy Cache Server Performance Model with the Probabilistic Model Checker PRISM}},
booktitle = {{WWV'09, 5th Int'l Workshop on Automated Specification and Verification of Web Systems}},
language = {english},
abstract = {We report our experience with formulating and analyzing in the probabilisticmodel checker PRISM a web server performance model with proxy cacheserver that was previously described in the literature in terms of classical queuingtheory. By our work various ambiguities and deficiencies (also errors) arerevealed; in particular, it is not clear how the reported paper simulates the networkbandwidth, as a queue or a delay. To avoid such ambiguities we argue thatnowadays performance modeling should make use of (at least be accompaniedby) state machine descriptions such as those used by PRISM. On the one hand,this helps to more accurately describe the systems whose performance are to bemodeled (by making hidden assumptions explicit) and give more useful informationfor the concrete implementation of these models (appropriate buffer sizes).On the other hand, since probabilistic model checkers such as PRISM are furthermoreable to analyze such models automatically, analytical models can bevalidated by corresponding experiments which helps to increase},
pages = {--},
address = {Hagenberg, Austria},
isbn_issn = {-},
year = {2009},
month = {July},
editor = {Demis Ballis and Temur Kutsia},
refereed = {yes},
sponsor = {Supported by the Austrian-Hungarian Scientific/Technical Cooperation Contract HU 13/2007},
length = {15}
}

2008

[Guta]

Analyzing Web Server Performance Models with the Probabilistic Model Checker PRISM

Tamas Berczes, Gabor Guta, Gabor Kusper, Wolfgang Schreiner, Janos Sztrik

Technical report no. 08-17 in RISC Report Series, Research Institute for Symbolic Computation (RISC), Johannes Kepler University Linz, Austria. ISSN 2791-4267 (online). November 2008. [pdf]
[bib]
@techreport{RISC3522,
author = {Tamas Berczes and Gabor Guta and Gabor Kusper and Wolfgang Schreiner and Janos Sztrik},
title = {{Analyzing Web Server Performance Models with the Probabilistic Model Checker PRISM}},
language = {english},
abstract = {We report our experience with formulating and analyzing in the probabilisticmodel checker PRISM various closely related web server performance models thatwere previously described in literature in terms of classical queuingtheory. By our work various ambiguities and deficiencies (alsoerrors) are revealed; in particular, the PRISM models which combine statemachines descriptions with performance characteristics show that the originaldescriptions used slightly differed assumptions for their analysis.Furthermore, while the queuing models are typically based on infinite queues,the state spaces of the PRISM models have to be finite for an automatedanalysis. While this forces us to explicitly deal with buffer overflows, italso gives us the possibility to investigate appropriate buffer sizes forconcrete implementations of the models. Although also one of the previouslyreported models used a finite queue in some place, our investigations revealthat the size of that queue is actually not critical, while another(previously not constrained) one is.Based on these observations, we argue that nowadays performance modelingshould make use of (at least be accompanied by) state machine descriptionssuch as those used by PRISM. On the one hand, this helps to more accuratelydescribe the systems whose performance are to be modeled (by making hiddenassumptions explicit) and give more useful information for the concreteimplementation of these models (appropriate buffer sizes). On the other hand,since probabilistic model checkers such as PRISM are furthermore able toanalyze such models automatically, analytical models can be validated bycorresponding experiments which helps to increase the trust into the adequacyof these models and their real-world interpretation},
number = {08-17},
year = {2008},
month = {November},
sponsor = {Austrian-Hungarian Scientific/Technical Cooperation Contract HU 13/2007},
length = {73},
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)}
}

2007

[Guta]

Comparing the Performance Modeling Environment MOSEL and the Probabilistic Model Checker PRISM for Modeling and Analyzing Retrial Queueing Systems

Tamas Berczes, Gabor Guta, Gabor Kusper, Wolfgang Schreiner, Janos Sztrik

Technical report no. 07-17 in RISC Report Series, Research Institute for Symbolic Computation (RISC), Johannes Kepler University Linz, Austria. ISSN 2791-4267 (online). December 2007. Project Report. [pdf]
[bib]
@techreport{RISC3369,
author = {Tamas Berczes and Gabor Guta and Gabor Kusper and Wolfgang Schreiner and Janos Sztrik},
title = {{Comparing the Performance Modeling Environment MOSEL and the Probabilistic Model Checker PRISM for Modeling and Analyzing Retrial Queueing Systems}},
language = {english},
abstract = {We describe the results of analyzing the performance model of a retrialqueueing system with the probabilistic model checker PRISM. The systemhas been previously analyzed with the help of the performance modeling environmentMOSEL; we are able to accurately reproduce the results reportedin literature. Furthermore, we compare PRISM and MOSEL with respect totheir modeling languages and ways of specifying performance queries andbenchmark the executions of the tools.},
number = {07-17},
year = {2007},
month = {December},
sponsor = {Austrian-Hungarian Scientific/Technical Cooperation Contract HU 13/2007},
length = {40},
type = {Project Report},
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)}
}

Loading…