Esper K (2026)
Publication Language: English
Publication Type: Thesis
Publication year: 2026
URI: https://open.fau.de/handle/openfau/40408
Multi-Processor Systems-on-Chip (MPSoC) platforms have become popular for executing embedded applications in various domains such as consumer electronics and automotive systems. Such embedded applications often come with a set of Non-Functional Properties (NFPs), e.g., latency or power consumption, on which requirements are typically defined. These Non-Functional Requirements (NFRs) can be specified by a lower and an upper bound defining a corridor of proper values. However, meeting such NFRs is considered a difficult problem due to environment uncertainties caused by, e.g., varying inputs and/or overhead (exogenously). In addition, other uncertainties can arise endogenously, e.g., by dynamic power management components inside the MPSoC, which varies the number of active cores and/or their voltage/frequency level. As a remedy, Runtime Requirement Enforcement (RRE) techniques have been proposed that use system control knobs, e.g., voltage/frequency settings, to steer the execution properties within given requirement corridors. However, no formal proofs of enforcement techniques to guard requirements have been investigated prior to this thesis. This thesis is motivated by the need to develop RREs techniques that allow to apply formal rather than trace-based analysis regarding the satisfaction of a given set of NFRs. Moreover, providing a probabilistic analysis of the number or amount of possible requirement violations could be more useful than only reasoning about worst-case scenarios. In this thesis, Finite State Machines (FSMs) are used to formally model both enforcement strategies and system responses (feedback), and Discrete-Time Markov Chains (DTMCs) are introduced to model any environmental uncertainties. In addition, different forms of verification goals on the given set of requirements are proposed to be analyzed and used to compare different enforcement strategies for strict NFRs (that must never be violated) and for loose NFRs (that may be violated at times). Based on such a formalization, model checking techniques are shown to be applicable to verify enforcement strategies based on given verification goals. However, it is still not understood how to automatically design enforcement strategies for which it is possible to provide formal guarantees regarding the satisfaction of given verification goals and how to possibly treat conflicting verification goals, e.g., minimizing latency while reducing energy consumption. Moreover, probabilistic verification goals can be very beneficial in offering a quantitative analysis of different enforcement strategies when meeting one or more NFRS cannot always be guaranteed. Therefore, this thesis will address the problem of automatic synthesis of enforcement FSMs for which probabilities to meet a given set of different verification goals are optimized. As verification goals are usually conflicting, this problem is considered as a Multi-Objective Optimization (MOO) problem that typically delivers multiple Pareto-optimal solutions. For this, three synthesis approaches are proposed. The first method is a Design Space Exploration (DSE) approach based on Genetic Algorithms (GAs), while the second is based on Reinforcement Learning (RL), and the last one is an approach that combines both of GAs and RL. Finally, enforcement strategies can be classified to either prohibit proactively a requirement violation or to react to a violation. Initial ideas on enforcement techniques were only able to distinguish which requirement bounds are satisfied and which are violated and then react accordingly. As a generalization, this thesis proposes enforcement strategies that are able to react according to the amount of violation of a lower or upper bound, resulting into a finer-grained reaction. For this, user-given corridors are partitioned into response ranges (i.e., sub-corridors) of NFPs responses on which the reaction will be differentiated. Here, three methods are proposed. The first one is a DSE that searches for such response ranges while simultaneously optimizing enforcement FSMs, which typically yields a large search space. Therefore, two heuristics are additionally proposed that statically compute candidate response ranges before a DSE starts to optimize enforcement FSMs. In summary, the presented enforcement methodology enables the verification of NFRs of programs on MPSoCs under exogeneous and endogenous environments. As many of these NFRs are related to safety properties, it is interesting to formally investigate how far this methodology can be applied to safety-critical applications. Therefore, an application and extension of the presented methodology using enforcement FSMs is presented with a focus on the domain of Human-Robot Interaction (HRI), in which collision avoidance is considered as a safety requirement to be enforced.
APA:
Esper, K. (2026). Enforcement of Non-Functional Execution Properties of Programs on MPSoCs using Finite State Machines (Dissertation).
MLA:
Esper, Khalil. Enforcement of Non-Functional Execution Properties of Programs on MPSoCs using Finite State Machines. Dissertation, 2026.
BibTeX: Download