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

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