Formal Parameter Synthesis for Energy-Utility-Optimal Fault Tolerance

Publikation: Beitrag in Buch/Konferenzbericht/Sammelband/GutachtenBeitrag in KonferenzbandBeigetragenBegutachtung

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.

Details

OriginalspracheEnglisch
TitelComputer Performance Engineering
Redakteure/-innenRena Bakhshi, Paolo Ballarini, Benoît Barbot, Hind Castel-Taleb, Anne Remke
Herausgeber (Verlag)Springer, Berlin [u. a.]
Seiten78-93
Seitenumfang16
ISBN (Print)978-3-030-02226-6
PublikationsstatusVeröffentlicht - 2018
Peer-Review-StatusJa

Publikationsreihe

ReiheLecture Notes in Computer Science, Volume 11178
ISSN0302-9743

Workshop

Titel15th European Performance Engineering Workshop
KurztitelEPEW 2018
Veranstaltungsnummer
Dauer29 - 30 Oktober 2018
Webseite
BekanntheitsgradInternationale Veranstaltung
Ort
StadtParis
LandFrankreich

Externe IDs

Scopus 85055550683
ORCID /0000-0002-5321-9343/work/142236717
ORCID /0000-0003-1724-2586/work/165453590

Schlagworte

Schlagwörter

  • Probabilistic model checking, Redone, Checking Data Flow (DFC), Computer-algebra Techniques, Transaction Length

Bibliotheksschlagworte