Evaluating Process Algebra Models versus State-oriented Models [85öu8]

@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 onevaluating the response times of client/server system models. In earlier work, we describedsuch systems by queue models where only the number of pending requests was stored andmeasured. 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 theninvestigate various possibilities how times can be directly measured in PRISM in continuousand discrete time models and in this process also investigate various features that have beenintroduced in the new version 4.0 of PRISM that were not yet available for our earlierwork. Finally, we apply our insights to measuring time explicitly in client/server modelsand 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}
}

@techreport{RISC4749,
author = {Wolfgang Schreiner and Nikolaj Popov and Tamas Berczes and Janos Sztrik and Gabor Kusper},
title = {{Applying High Performance Computing to Analyzing by Probabilistic Model Checking Mobile Cellular Networks with Spectrum Renting}},
language = {english},
abstract = {We report on the use of high performance computing in order to analyze with the proba-bilistic model checker PRISM mobile cellular networks, in particular the system describedin the paper “A New Finite-Source Queueing Model for Mobile Cellular Networks Apply-ing Spectrum Renting” by Tien v. Do et al. That paper proposes a new finite-source retrialqueueing model to consider spectrum renting in mobile cellular networks; numerical re-sults are there produced with the MOSEL-2 tool. Our results show that the model can bealso appropriately described and analyzed in PRISM, but that modeling becomes compar-atively more cumbersome due to the lack of zero-time/infinite-rate transitions in PRISM.By using a massively parallel non-uniform memory architecture (NUMA), we are able toconsiderably speed up the analysis of large scale models.},
year = {2013},
month = {July},
institution = {Research Institute for Symbolic Computation (RISC), Johannes Kepler University, Linz, Austria},
keywords = {performance modeling, probabilistic model checking, parallel computing},
sponsor = {Supported by the European project FIRST (TÁMOP-4.4.2.C) and by the project 85öu8 of the Stiftung Aktion Österreich-Ungarn},
length = {24}
}