摘要: When designing embedded systems, engineers have to consider nonfunctional requirements, such as real-time or energy consumption constraints. To enforce or counteract any potential violation of such constraints, feedback-based cont... 展开 When designing embedded systems, engineers have to consider nonfunctional requirements, such as real-time or energy consumption constraints. To enforce or counteract any potential violation of such constraints, feedback-based control techniques can be applied, e.g., adapting the degree of parallelism or changing the DVFS settings of the resources. Of particular interest here are formal techniques for proving that the developed controllers either never lead to a violation of a given set of non-functional requirements or minimize the probability of such violations occurring. In the context of run-time requirement enforcement, it has been shown that either property can be described as one or a set of verification goals of a given or generated enforcement strategy. In this paper, we propose a design space exploration(DSE) methodology to determine a Pareto-optimal set of verifiable FSM-based feedback-based enforcers for a given set of verification goals. A major problem encountered here is that formally checking a set of verification goals can be quite time-intensive and, as a consequence, may lead to intolerably high exploration times. As a remedy, this paper proposes a hybrid DSE methodology based on a combination of multi-objective evolutionary algorithm search and reinforcement learning (RL).In particular, RL is used in each iteration of the evolutionary algorithm as a local search strategy to efficiently identify and fill gaps of diversity in the front of non-dominated solutions. It is shown that this leads to drastic reductions in exploration time. In three case studies, we compare the proposed approach with state-of-the-art methods and demonstrate considerably smaller optimization times alongside its capability to generate controllers exhibiting higher probabilities of satisfying a given set of requirement verification goals, as verified by model checkers.CCS CONCEPTS•Computer systems organization $\rightarrow$ Self-organizing autonomic computing;•Theory of computation $\rightarrow$ Modal and temporal logics; Verification by model checking;•Mathematics of computing $\rightarrow$ Probabilistic representations. 收起