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

Project Lead

Project Duration

01/10/2012 - 30/09/2013

Project URL

Go to Website

Publications

2013

Project "85öu8": Final Report - Evaluating Process Algebra Models versus State-oriented Models for the Performance Analysis of Real-time Systems and Software Designs

Janos Sztrik, Wolfgang Schreiner, Tamas Berczes, Gabor Kusper, Nikolaj Popov

Technical report no. 13-08 in RISC Report Series, Research Institute for Symbolic Computation (RISC), Johannes Kepler University Linz, Schloss Hagenberg, 4232 Hagenberg, Austria. September 2013.
[bib]
@techreport{RISC4817,
author = {Janos Sztrik and Wolfgang Schreiner and Tamas Berczes and Gabor Kusper and Nikolaj Popov},
title = {{Project "85öu8": Final Report - Evaluating Process Algebra Models versus State-oriented Models for the Performance Analysis of Real-time Systems and Software Designs}},
language = {english},
number = {13-08},
year = {2013},
month = {September},
length = {0},
type = {RISC Report Series},
institution = {Research Institute for Symbolic Computation (RISC), Johannes Kepler University Linz},
address = {Schloss Hagenberg, 4232 Hagenberg, Austria}
}

Experiments with Measuring Time in PRISM 4.0

Wolfgang Schreiner

Research Institute for Symbolic Computation (RISC), Johannes Kepler University, Linz, Austria. Technical report, March 2013. Technical Report. [pdf]
[bib]
@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}
}

Applying High Performance Computing to Analyzing by Probabilistic Model Checking Mobile Cellular Networks with Spectrum Renting

Wolfgang Schreiner, Nikolaj Popov, Tamas Berczes, Janos Sztrik, Gabor Kusper

Research Institute for Symbolic Computation (RISC), Johannes Kepler University, Linz, Austria. Technical report, July 2013. [pdf]
[bib]
@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}
}

Loading…