RISC JKU
  • @techreport{RISC5595,
    author = {Wolfgang Schreiner and Tamás Bérczes and János Sztrik and Hamza Nemouchi},
    title = {{On the Probabilistic Model Checking of Cognitive Radio Networks and Cognitive Infocommunication Systems}},
    language = {english},
    abstract = {We report on the usage of the probabilistic model checker PRISM to validate respectively falsify previously published results on the performance of cognitive radio networks and other cognitive infocommunication systems. For this purpose, we construct formal system models in the PRISM modeling language as Continuous Time Markov Chains (CTMCs) that are analyzed with the help of queries formulated in a variant of continuous stochastic logic (CSL). It is shown that many results can be accurately reproduced but also that a few previously reported results are clearly erroneous. Furthermore, we report several deviations from previously reported results where the reasons are unclear and need further investigation. Here a major problem is that the systems that have been analyzed in literature are usually just described in informal language which leaves ample room for interpretation. This makes the reconstruction of corresponding formal system models and the reproduction of performance measures a difficult task and limits the long-term scientific value of the reported results.},
    number = {18-04},
    year = {2018},
    month = {February},
    keywords = {formal methods, performance analysis, queueing systems},
    sponsor = {Supported by the Stiftung Aktion Österreich-Ungarn project 96öu8 “Engineering Information Technology Modelling and Design of Cognitive Radio Networks”},
    length = {24},
    type = {RISC Report Series},
    institution = {Research Institute for Symbolic Computation (RISC), Johannes Kepler University Linz},
    address = {Altenberger Straße 69, 4040 Linz, Austria},
    issn = {2791-4267 (online)}
    }