@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 probabilistic
model checker PRISM a web server performance model with proxy cache
server that was previously described in the literature in terms of classical queuing
theory. By our work various ambiguities and deficiencies (also errors) are
revealed; in particular, it is not clear how the reported paper simulates the network
bandwidth, as a queue or a delay. To avoid such ambiguities 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},
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}
}