RISC RISC Research Institute for Symbolic Computation  
  • @techreport{RISC4684,
    author = {Wolfgang Schreiner},
    title = {{Experiments with Measuring Time in PRISM 4.0}},
    language = {english},
    abstract = {We report on experiments with the probabilistic symbol model checker PRISM 4.0 on evaluating the response times of client/server system models. In earlier work, we described such systems by queue models where only the number of pending requests was stored and measured. Under certain assumptions, we could then apply results from queueing theory (Little’s Law) to derive the time that a request spends until getting processed. In this report, we first revisit this approach and substantiate it by a more detailed analytic analysis. We then investigate various possibilities how times can be directly measured in PRISM in continuous and discrete time models and in this process also investigate various features that have been introduced in the new version 4.0 of PRISM that were not yet available for our earlier work. Finally, we apply our insights to measuring time explicitly in client/server models and compare the results to those that we have previously derived by indirect means.},
    year = {2013},
    month = {March},
    institution = {Research Institute for Symbolic Computation (RISC), Johannes Kepler University, Linz, Austria},
    sponsor = {Project 85öu8 of the Stiftung Aktion Österreich-Ungarn},
    length = {60},
    type = {Technical Report}