License: Creative Commons Attribution 4.0 International license (CC BY 4.0)
When quoting this document, please refer to the following
DOI: 10.4230/OASIcs.NG-RES.2023.7
URN: urn:nbn:de:0030-drops-177380
URL: http://dagstuhl.sunsite.rwth-aachen.de/volltexte/2023/17738/
Go to the corresponding OASIcs Volume Portal

Esper, Khalil ; Spieck, Jan ; Sixdenier, Pierre-Louis ; Wildermann, Stefan ; Teich, Jürgen

RAVEN: Reinforcement Learning for Generating Verifiable Run-Time Requirement Enforcers for MPSoCs

pdf-format:
OASIcs-NG-RES-2023-7.pdf (0.9 MB)

Abstract

In embedded systems, applications frequently have to meet non-functional requirements regarding, e.g., real-time or energy consumption constraints, when executing on a given MPSoC target platform.
Feedback-based controllers have been proposed that react to transient environmental factors by adapting the DVFS settings or degree of parallelism following some predefined control strategy. However, it is, in general, not possible to give formal guarantees for the obtained controllers to satisfy a given set of non-functional requirements. Run-time requirement enforcement has emerged as a field of research for the enforcement of non-functional requirements at run-time, allowing to define and formally verify properties on respective control strategies specified by automata. However, techniques for the automatic generation of such controllers have not yet been established.
In this paper, we propose a technique using reinforcement learning to automatically generate verifiable feedback-based enforcers. For that, we train a control policy based on a representative input sequence at design time. The learned control strategy is then transformed into a verifiable enforcement automaton which constitutes our run-time control model that can handle unseen input data. As a case study, we apply the approach to generate controllers that are able to increase the probability of satisfying a given set of requirement verification goals compared to multiple state-of-the-art approaches, as can be verified by model checkers.

BibTeX - Entry

@InProceedings{esper_et_al:OASIcs.NG-RES.2023.7,
  author =	{Esper, Khalil and Spieck, Jan and Sixdenier, Pierre-Louis and Wildermann, Stefan and Teich, J\"{u}rgen},
  title =	{{RAVEN: Reinforcement Learning for Generating Verifiable Run-Time Requirement Enforcers for MPSoCs}},
  booktitle =	{Fourth Workshop on Next Generation Real-Time Embedded Systems (NG-RES 2023)},
  pages =	{7:1--7:16},
  series =	{Open Access Series in Informatics (OASIcs)},
  ISBN =	{978-3-95977-268-6},
  ISSN =	{2190-6807},
  year =	{2023},
  volume =	{108},
  editor =	{Terraneo, Federico and Cattaneo, Daniele},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/opus/volltexte/2023/17738},
  URN =		{urn:nbn:de:0030-drops-177380},
  doi =		{10.4230/OASIcs.NG-RES.2023.7},
  annote =	{Keywords: Verification, Runtime Requirement Enforcement, Reinforcement Learning}
}

Keywords: Verification, Runtime Requirement Enforcement, Reinforcement Learning
Collection: Fourth Workshop on Next Generation Real-Time Embedded Systems (NG-RES 2023)
Issue Date: 2023
Date of publication: 16.03.2023

DROPS-Home | Fulltext Search | Imprint | Privacy Published by LZI