Formal Parameter Synthesis for Energy-Utility-Optimal Fault Tolerance

Linda HerrmannLinda Herrmann, Christel BaierChristel Baier, Christof FetzerChristof Fetzer, Sascha KlüppelholzSascha Klüppelholz, Markus NapierkowskiMarkus Napierkowski

DOI Link

Linda Herrmann, Christel Baier, Christof Fetzer, Sascha Klüppelholz, Markus Napierkowski
Formal Parameter Synthesis for Energy-Utility-Optimal Fault Tolerance
Proc. of 15th European Workshop on Computer Performance Engineering (EPEW), volume 11178 of Lecture Notes in Computer Science, 78--93. Springer

Details
Bibtex

KurzfassungAbstract
Fault-tolerance techniques are widely used to improve the resiliency of hardware/software systems. An important step for the deployment of such techniques in a concrete setting is to find reasonable configurations balancing the tradeoff between resiliency and energy. The paper reports on a case study where we employ probabilistic model checking to synthesize values for tunable system parameters of a redo-based fault-tolerance mechanism. We consider discrete parameters of a finite range (as the number of redos) as well as continuous parameters to encode the error detection rates of the underlying control- and data-flow checkers. To tackle the state-explosion problem, we exploit structural properties of redo-based protocols. The parameter synthesis approach combines probabilistic model checking for Markov chains with parametric transition probabilities and reward values and computer-algebra techniques to determine parameter valuations that minimize the expected overhead given constraints on the utility, depending on a given error probability.
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-030-02227-3_6.

@inproceedings{HBFKN,
  author    = {Linda Herrmann and Christel Baier and Christof Fetzer and Sascha
               Kl{\"{u}}ppelholz and Markus Napierkowski},
  title     = {Formal Parameter Synthesis for Energy-Utility-Optimal Fault
               Tolerance},
  booktitle = {Proc. of 15th European Workshop on Computer Performance
               Engineering (EPEW)},
  series    = {Lecture Notes in Computer Science},
  volume    = {11178},
  publisher = {Springer},
  pages     = {78--93},
  doi       = {10.1007/978-3-030-02227-3_6}
}