Performance Analysis of Real-time Systems and Software Designs [HU 10/2012]
Project Lead
Project Duration
01/12/2012 - 30/11/2014Project URL
Go to WebsitePublications
2014
[Schreiner]
Probabilistic Model Checking on HPC Systems for the Performance Analysis of Mobile Networks
Wolfgang Schreiner, Tamas Berczes, Janos Sztrik
Annales Mathematicae et Informaticae 43, pp. 123-144. 2014. Líceum University Press, ISSN 1787-5021, ISSN 1787-6117.@article{RISC5058,
author = {Wolfgang Schreiner and Tamas Berczes and Janos Sztrik},
title = {{Probabilistic Model Checking on HPC Systems for the Performance Analysis of Mobile Networks}},
language = {english},
abstract = {We report on the use of HPC resources for the performance analysis of the mobilecellular network model described in “A New Finite-Source Queueing Model forMobile Cellular Networks Applying Spectrum Renting” by Tien Van Do et al. Thatpaper proposed a new finite-source retrial queueing model with spectrum renting thatwas analyzed with the MOSEL-2 tool. Our results show how this model can be alsoappropriately described and analyzed with the probabilistic model checker PRISM, althoughat some cost considering the formulation of the model; in particular, we are ableto accurately reproduce most of the analytical results presented in that paper and thusincrease the confidence in the previously presented results. However, we also outlinesome discrepancies which may hint to deficiencies of the original analysis. Moreover,by applying a parallel computing framework developed for this purpose, we are ableto considerably speed up studies performed with the PRISM tool. The investigationsare illustrated by figures and conclusions are drawn.},
journal = {Annales Mathematicae et Informaticae},
volume = {43},
pages = {123--144},
publisher = {Líceum University Press},
isbn_issn = {ISSN 1787-5021, ISSN 1787-6117},
year = {2014},
refereed = {yes},
length = {22}
}
author = {Wolfgang Schreiner and Tamas Berczes and Janos Sztrik},
title = {{Probabilistic Model Checking on HPC Systems for the Performance Analysis of Mobile Networks}},
language = {english},
abstract = {We report on the use of HPC resources for the performance analysis of the mobilecellular network model described in “A New Finite-Source Queueing Model forMobile Cellular Networks Applying Spectrum Renting” by Tien Van Do et al. Thatpaper proposed a new finite-source retrial queueing model with spectrum renting thatwas analyzed with the MOSEL-2 tool. Our results show how this model can be alsoappropriately described and analyzed with the probabilistic model checker PRISM, althoughat some cost considering the formulation of the model; in particular, we are ableto accurately reproduce most of the analytical results presented in that paper and thusincrease the confidence in the previously presented results. However, we also outlinesome discrepancies which may hint to deficiencies of the original analysis. Moreover,by applying a parallel computing framework developed for this purpose, we are ableto considerably speed up studies performed with the PRISM tool. The investigationsare illustrated by figures and conclusions are drawn.},
journal = {Annales Mathematicae et Informaticae},
volume = {43},
pages = {123--144},
publisher = {Líceum University Press},
isbn_issn = {ISSN 1787-5021, ISSN 1787-6117},
year = {2014},
refereed = {yes},
length = {22}
}
[Schreiner]
Analyzing Cluster Scheduling Schemes by Probabilistic Model Checking
Wolfgang Schreiner, Tamas Berczes, Adam Toth
Research Institute for Symbolic Computation (RISC), Johannes Kepler University, Linz, Austria. Technical report, September 2014. [pdf]@techreport{RISC5059,
author = {Wolfgang Schreiner and Tamas Berczes and Adam Toth},
title = {{Analyzing Cluster Scheduling Schemes by Probabilistic Model Checking}},
language = {english},
abstract = {We report in this paper on initial results of modeling and analyzing with the probabilisticmodel checker PRISM various cluster scheduling schemes that were introduced by Do, Vu,Tran, and Nguyen in their paper “A generalized model for investigating scheduling schemesin computational clusters” and analyzed by simulation there. The preliminary results areencouraging, but there also remain some open issues that need to be addressed.},
year = {2014},
month = {September},
institution = {Research Institute for Symbolic Computation (RISC), Johannes Kepler University, Linz, Austria},
sponsor = {Supported by the project HU 10/2012 of the Austrian Academic Exchange Service (ÖAD) and by the TÁMOP- 4.2.2.C-11/1/KONV-2012-0001 project.},
length = {41}
}
author = {Wolfgang Schreiner and Tamas Berczes and Adam Toth},
title = {{Analyzing Cluster Scheduling Schemes by Probabilistic Model Checking}},
language = {english},
abstract = {We report in this paper on initial results of modeling and analyzing with the probabilisticmodel checker PRISM various cluster scheduling schemes that were introduced by Do, Vu,Tran, and Nguyen in their paper “A generalized model for investigating scheduling schemesin computational clusters” and analyzed by simulation there. The preliminary results areencouraging, but there also remain some open issues that need to be addressed.},
year = {2014},
month = {September},
institution = {Research Institute for Symbolic Computation (RISC), Johannes Kepler University, Linz, Austria},
sponsor = {Supported by the project HU 10/2012 of the Austrian Academic Exchange Service (ÖAD) and by the TÁMOP- 4.2.2.C-11/1/KONV-2012-0001 project.},
length = {41}
}
[Schreiner]
Analyzing the Energy Efficiency of Cluster Scheduling Schemes by Probabilistic Model Checking
Wolfgang Schreiner, Tamas Berczes, Adam Toth
Research Institute for Symbolic Computation (RISC), Johannes Kepler University, Linz, Austria. Technical report, December 2014. [pdf]@techreport{RISC5084,
author = {Wolfgang Schreiner and Tamas Berczes and Adam Toth},
title = {{Analyzing the Energy Efficiency of Cluster Scheduling Schemes by Probabilistic Model Checking}},
language = {english},
abstract = {We report in this paper on our results of modeling and analyzing with theprobabilistic model checker PRISM the energy efficiency of various clusterscheduling schemes. These schemes were originallyintroduced by Do, Vu, Tran, and Nguyen in theirpaper "A generalized model for investigating scheduling schemes incomputational clusters" and analyzed by simulation there. Our investigationswith PRISM validate the reported results and also subsequent results that were achieved with the performance analysis tool MOSEL-2.Furthermore, some measures that could be determined by simulation but not withMOSEL-2 could be also derived with PRISM.},
year = {2014},
month = {December},
institution = {Research Institute for Symbolic Computation (RISC), Johannes Kepler University, Linz, Austria},
keywords = {formal methods, performance analysis, energy analysis},
sponsor = {Supported by the project HU 10/2012 of the Austrian Academic Exchange Service (ÖAD) and by the TÁMOP- 4.2.2.C-11/1/KONV-2012-0001 project.},
length = {29}
}
author = {Wolfgang Schreiner and Tamas Berczes and Adam Toth},
title = {{Analyzing the Energy Efficiency of Cluster Scheduling Schemes by Probabilistic Model Checking}},
language = {english},
abstract = {We report in this paper on our results of modeling and analyzing with theprobabilistic model checker PRISM the energy efficiency of various clusterscheduling schemes. These schemes were originallyintroduced by Do, Vu, Tran, and Nguyen in theirpaper "A generalized model for investigating scheduling schemes incomputational clusters" and analyzed by simulation there. Our investigationswith PRISM validate the reported results and also subsequent results that were achieved with the performance analysis tool MOSEL-2.Furthermore, some measures that could be determined by simulation but not withMOSEL-2 could be also derived with PRISM.},
year = {2014},
month = {December},
institution = {Research Institute for Symbolic Computation (RISC), Johannes Kepler University, Linz, Austria},
keywords = {formal methods, performance analysis, energy analysis},
sponsor = {Supported by the project HU 10/2012 of the Austrian Academic Exchange Service (ÖAD) and by the TÁMOP- 4.2.2.C-11/1/KONV-2012-0001 project.},
length = {29}
}
2013
[Kusper]
A Case Study on Exploring the Performance Limits of PRISM
Wolfgang Schreiner, Tamas Berczes, Janos Sztrik, Gabor Kusper
Research Institute for Symbolic Computation (RISC), Johannes Kepler University, Linz, Austria. Technical report, September 2013. [pdf]@techreport{RISC4820,
author = {Wolfgang Schreiner and Tamas Berczes and Janos Sztrik and Gabor Kusper},
title = {{A Case Study on Exploring the Performance Limits of PRISM}},
language = {english},
abstract = {We investigate based on a simple system model the range of applicability of the probabilisticmodel checker PRISM. In particular, we analyze the effect of the choice of thechecking engine, of the numerical equation solver, and of other settings on the time andmemory required for the analysis of the model by PRISM. The results demonstrate that notalways the same engine is the fastest one but that for large models an otherwise slow enginemay show superior performance; furthermore, the appropriate choice of the terminationcriterium can make the crucial difference between the success and the failure of an analysis.},
year = {2013},
month = {September},
institution = {Research Institute for Symbolic Computation (RISC), Johannes Kepler University, Linz, Austria},
length = {13}
}
author = {Wolfgang Schreiner and Tamas Berczes and Janos Sztrik and Gabor Kusper},
title = {{A Case Study on Exploring the Performance Limits of PRISM}},
language = {english},
abstract = {We investigate based on a simple system model the range of applicability of the probabilisticmodel checker PRISM. In particular, we analyze the effect of the choice of thechecking engine, of the numerical equation solver, and of other settings on the time andmemory required for the analysis of the model by PRISM. The results demonstrate that notalways the same engine is the fastest one but that for large models an otherwise slow enginemay show superior performance; furthermore, the appropriate choice of the terminationcriterium can make the crucial difference between the success and the failure of an analysis.},
year = {2013},
month = {September},
institution = {Research Institute for Symbolic Computation (RISC), Johannes Kepler University, Linz, Austria},
length = {13}
}
[Schreiner]
Initial Results on Modeling in PRISM Mobile Cellular Networks with Spectrum Renting
Wolfgang Schreiner
Research Institute for Symbolic Computation (RISC), Johannes Kepler University, Linz, Austria. Technical report, April 9 2013. [pdf]@techreport{RISC4705,
author = {Wolfgang Schreiner},
title = {{Initial Results on Modeling in PRISM Mobile Cellular Networks with Spectrum Renting}},
language = {english},
abstract = {We report in this paper on our initial results on modeling in theprobabilistic model checker PRISM the systemdescribed in the paper \enquote{A New Finite-Source Queueing Model forMobile Cellular Networks Applying Spectrum Renting} by Tien v. Do et al.That paper proposes a new finite-source retrial queueing model to considerspectrum renting in mobile cellular networks; numerical results are there producedwith the MOSEL-2 tool. Our results show that the model can be described andanalyzed in PRISM in a very transparent way; however, due to an apparent system bug we are not yet able to check models of the same sizeas in MOSEL-2.},
year = {2013},
month = {April 9},
institution = {Research Institute for Symbolic Computation (RISC), Johannes Kepler University, Linz, Austria},
sponsor = {Supported by the project HU 10/2012 of the Austrian Academic Exchange Service (ÖAD).},
length = {18}
}
author = {Wolfgang Schreiner},
title = {{Initial Results on Modeling in PRISM Mobile Cellular Networks with Spectrum Renting}},
language = {english},
abstract = {We report in this paper on our initial results on modeling in theprobabilistic model checker PRISM the systemdescribed in the paper \enquote{A New Finite-Source Queueing Model forMobile Cellular Networks Applying Spectrum Renting} by Tien v. Do et al.That paper proposes a new finite-source retrial queueing model to considerspectrum renting in mobile cellular networks; numerical results are there producedwith the MOSEL-2 tool. Our results show that the model can be described andanalyzed in PRISM in a very transparent way; however, due to an apparent system bug we are not yet able to check models of the same sizeas in MOSEL-2.},
year = {2013},
month = {April 9},
institution = {Research Institute for Symbolic Computation (RISC), Johannes Kepler University, Linz, Austria},
sponsor = {Supported by the project HU 10/2012 of the Austrian Academic Exchange Service (ÖAD).},
length = {18}
}
[Schreiner]
Experiments with Measuring Time in PRISM 4.0 (Addendum)
Wolfgang Schreiner
Research Institute for Symbolic Computation (RISC), Johannes Kepler University, Linz, Austria. Technical report, April 2013. [pdf]@techreport{RISC4701,
author = {Wolfgang Schreiner},
title = {{Experiments with Measuring Time in PRISM 4.0 (Addendum)}},
language = {english},
abstract = { 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 TimedAutomata (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 theanalysis 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 timeanalysis by explicit time measurement in PRISM is more complex than previously thoughtsuch that the application of Little’s Law still has its merit.},
year = {2013},
month = {April},
institution = {Research Institute for Symbolic Computation (RISC), Johannes Kepler University, Linz, Austria},
keywords = {Supported by the project HU 10/2012 of the Austrian Academic Exchange Service (ÖAD).},
length = {14}
}
author = {Wolfgang Schreiner},
title = {{Experiments with Measuring Time in PRISM 4.0 (Addendum)}},
language = {english},
abstract = { 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 TimedAutomata (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 theanalysis 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 timeanalysis by explicit time measurement in PRISM is more complex than previously thoughtsuch that the application of Little’s Law still has its merit.},
year = {2013},
month = {April},
institution = {Research Institute for Symbolic Computation (RISC), Johannes Kepler University, Linz, Austria},
keywords = {Supported by the project HU 10/2012 of the Austrian Academic Exchange Service (ÖAD).},
length = {14}
}
