@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 probabilistic
model checker PRISM various closely related web server performance models that
were previously described in literature in terms of classical queuing
theory. By our work various ambiguities and deficiencies (also
errors) are revealed; in particular, the PRISM models which combine state
machines descriptions with performance characteristics show that the original
descriptions 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 automated
analysis. While this forces us to explicitly deal with buffer overflows, it
also gives us the possibility to investigate appropriate buffer sizes for
concrete implementations of the models. Although also one of the previously
reported models used a finite queue in some place, our investigations reveal
that 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 modeling
should make use of (at least be accompanied by) 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 be modeled (by making hidden
assumptions explicit) and give more useful information for the concrete
implementation of these models (appropriate buffer sizes). On the other hand,
since probabilistic model checkers such as PRISM are furthermore able to
analyze such models automatically, analytical models can be validated by
corresponding experiments which helps to increase the trust into the adequacy
of 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)}
}