Esper K, Teich J (2024)
Publication Language: English
Publication Type: Conference contribution, Conference Contribution
Publication year: 2024
Publisher: Schloss Dagstuhl – Leibniz-Zentrum für Informatik
Series: Open Access Series in Informatics (OASIcs)
City/Town: Saarbrücken/Wadern
Book Volume: 117
Pages Range: 4:1-4:11
Conference Proceedings Title: Fifth Workshop on Next Generation Real-Time Embedded Systems (NG-RES 2024)
ISBN: 978-3-95977-313-3
URI: https://drops.dagstuhl.de/entities/document/10.4230/OASIcs.NG-RES.2024.4
DOI: 10.4230/OASIcs.NG-RES.2024.4
Embedded system applications usually have requirements regarding non-functional properties of their
execution like latency or power consumption. Enforcement of such requirements can be implemented
by a reactive control loop, where an enforcer determines based on a system response (feedback) how
to control the system, e.g., by selecting the number of active cores allocated to a program or by
scaling their voltage/frequency mode. It is of a particular interest to design enforcement strategies
for which it is possible to provide formal guarantees with respect to requirement violations, especially
under a largely varying environmental input (workload) per execution. In this paper, we consider
enforcement strategies that are modeled by a finite state machine (FSM) and the environment by
a discrete-time Markov chain. Such a formalization enables the formal verification of temporal
properties (verification goals) regarding the satisfaction of requirements of a given enforcement
strategy.
In this paper, we propose history-based enforcement FSMs which compute a reaction not just on
the current, but on a fixed history of K previously observed system responses. We then analyze the
quality of such enforcement FSMs in terms of the probability of satisfying a given set of verification
goals and compare them to enforcement FSMs that react solely on the current system response.
As experimental results, we present three use cases while considering requirements on latency and
power consumption. The results show that history-based enforcement FSMs outperform enforcement
FSMs that only consider the current system response regarding the probability of satisfying a given
set of verification goals.
APA:
Esper, K., & Teich, J. (2024). History-Based Run-Time Requirement Enforcement of Non-Functional Properties on MPSoCs. In Patrick Meumeu Yomsi, Stefan Wildermann (Eds.), Fifth Workshop on Next Generation Real-Time Embedded Systems (NG-RES 2024) (pp. 4:1-4:11). Munich, DE: Saarbrücken/Wadern: Schloss Dagstuhl – Leibniz-Zentrum für Informatik.
MLA:
Esper, Khalil, and Jürgen Teich. "History-Based Run-Time Requirement Enforcement of Non-Functional Properties on MPSoCs." Proceedings of the Fifth Workshop on Next Generation Real-Time Embedded Systems (NG-RES 2024), Munich Ed. Patrick Meumeu Yomsi, Stefan Wildermann, Saarbrücken/Wadern: Schloss Dagstuhl – Leibniz-Zentrum für Informatik, 2024. 4:1-4:11.
BibTeX: Download