"Experiments with Measuring Time in PRISM 4.0 (Addendum)"
, Serie RISC Report Series, RISC Hagenberg, Hagenberg, 4-2013
Experiments with Measuring Time in PRISM 4.0 (Addendum)
Sprache des Titels:
In our previous paper ?Experiments with Measuring Time in PRISM 4.0? we have re- ported on experiments with the probabilistic symbol model checker PRISM 4.0 on evalu- ating the response times of client/server system models. In that report some questions re- mained unresolved, in particular an unexpected result in the analysis of Probabilistic Timed Automata (PTA) in PRISM, and an unexplained discrepancy between explicit time mea- surement and results derived from queueing theory (by application of Little?s Law) in the analysis of a simple client/server model. In this addendum to that paper these open ques- tions are addressed and (essentially) solved. In particular, it is shown that expected time analysis by explicit time measurement in PRISM is more complex than previously thought such that the application of Little?s Law still has its merit.