Inproceedings3637339637: Unterschied zwischen den Versionen
Aus International Center for Computational Logic
Johannes Lehmann (Diskussion | Beiträge) (Die Seite wurde neu angelegt: „{{Publikation Erster Autor |ErsterAutorVorname=Linda |ErsterAutorNachname=Herrmann |FurtherAuthors=Christel Baier; Christof Fetzer; Sascha Klüppelholz; Markus Napierkowski}} {{Inproceedings |Booktitle=Proc. of 15th European Workshop on Computer Performance Engineering (EPEW) |Pages=78--93 |Publisher=Springer |Series=Lecture Notes in Computer Science |Title=Formal Parameter Synthesis for Energy-Utility-Optimal Fault Tolerance |Volume=11178 }}…“) |
Johannes Lehmann (Diskussion | Beiträge) K (Textersetzung - „Verifikation und formale quantitative Analyse“ durch „Algebraische und logische Grundlagen der Informatik“) |
||
| Zeile 14: | Zeile 14: | ||
|DOI Name=10.1007/978-3-030-02227-3_6 | |DOI Name=10.1007/978-3-030-02227-3_6 | ||
|Abstract=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. | |Abstract=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= | |Forschungsgruppe=Algebraische und logische Grundlagen der Informatik | ||
}} | }} | ||
Aktuelle Version vom 5. März 2025, 15:45 Uhr
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
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
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
- 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
@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}
}
