Energy-Utility Analysis for Resilient Systems Using Probabilistic Model Checking

Christel BaierChristel Baier, Clemens DubslaffClemens Dubslaff, Sascha KlüppelholzSascha Klüppelholz, Linda LeuschnerLinda Leuschner

DOI Link

Christel Baier, Clemens Dubslaff, Sascha Klüppelholz, Linda Leuschner
Energy-Utility Analysis for Resilient Systems Using Probabilistic Model Checking
Proc. of the 35th Conference on Application and Theory of Petri Nets and Concurrency (PETRI NETS), volume 8489 of Lecture Notes in Computer Science, 20--39, 2014. Springer

Details
Bibtex

KurzfassungAbstract
The automated quantitative system analysis in terms of probabilistic model checking (PMC) is nowadays well-established and has been applied successfully in various areas. Recently, we showed how PMC can be applied for the trade-off analysis between several cost and reward functions, such as energy and utility. Besides utility, also the resilience of a system, i.e., the systems capability to operate successfully even in unfavorable conditions, crucially depends on costs invested: It is well-known that better resilience can be achieved, e.g., through introducing redundant components, which however may yield higher energy consumption. In this paper, we focus on the interplay energy, utility and resilience. The formalization of the resulting trade-offs requires several concepts like quantiles, conditional probabilities and expectations and ratios of cost or reward functions. We present an overview how these quantitative measures for resilience mechanisms can be computed when the resilient systems are modeled either as discrete or continuous-time Markov chains. All the presented concepts of multi-objective reasoning are not supported by state-of-the-art probabilistic model checkers yet. By means of a small case study following the modular redundancy principle, we exemplify a resilience analysis within our prototype implementations.
Forschungsgruppe:Research Group: Algebraische und logische Grundlagen der InformatikAlgebraic and Logical Foundations of Computer Science

The final publication is available at Springer via http://dx.doi.org/10.1007/978-3-319-07734-5_2.

@inproceedings{BDKL2014,
  author    = {Christel Baier and Clemens Dubslaff and Sascha Kl{\"{u}}ppelholz
               and Linda Leuschner},
  title     = {Energy-Utility Analysis for Resilient Systems Using Probabilistic
               Model Checking},
  booktitle = {Proc. of the 35th Conference on Application and Theory of Petri
               Nets and Concurrency (PETRI {NETS)}},
  series    = {Lecture Notes in Computer Science},
  volume    = {8489},
  publisher = {Springer},
  year      = {2014},
  pages     = {20--39},
  doi       = {10.1007/978-3-319-07734-5_2}
}