Esper K, Wildermann S, Teich J (2021)

**Publication Language:** English

**Publication Type:** Conference contribution, Conference Contribution

**Publication year:** 2021

**Publisher:** Association for Computing Machinery

**Series:** MEMOCODE '21

**City/Town:** New York, NY, USA

**Pages Range:** 21–31

**Conference Proceedings Title:** Proceedings of the 19th ACM-IEEE International Conference on Formal Methods and Models for System Design

**ISBN:** 9781450391276

Many embedded system applications impose hard real-time, energy or safety requirements on corresponding programs typically concurrently executed on a given MPSoC target platform. Even when mutually isolating applications in space or time, the enforcement of such properties, e.g., by adjusting the number of processors allocated to a program or by scaling the voltage/frequency mode of involved processors, is a difficult problem to solve, particularly in view of typically largely varying environmental input (workload) per execution. In this paper, we formalize the related control problem using finite state machine models for the uncertain environment determining the workload, the system response (feedback), as well as the enforcer strategy. The contributions of this paper are as follows: a) Rather than trace-based simulation, the uncertain environment is modeled by a discrete-time Markov chain (DTMC) as a random process to characterize possible input sequences an application may experience. b) A number of important verification goals to analyze different enforcer FSMs are formulated in PCTL for the resulting stochastic verification problem, i.e., the likelihood of violating a timing or energy constraint, or the expected number of steps for a system to return to a given execution time corridor. c) Applying stochastic model checking, i.e., PRISM to analyze and compare enforcer FSMs in these properties, and finally d) proposing an approach for reducing the environment DTMC by partitioning equivalent environmental states (i.e., input states leading to an equal system response in each MPSoC mode) such that verification times can be reduced by orders of magnitude to just a few ms for real-world examples.

Khalil Esper
Sonderforschungsbereich/Transregio 89 Invasives Rechnen
Stefan Wildermann
Lehrstuhl für Informatik 12 (Hardware-Software-Co-Design)
Jürgen Teich
Lehrstuhl für Informatik 12 (Hardware-Software-Co-Design)

**APA:**

Esper, K., Wildermann, S., & Teich, J. (2021). Enforcement FSMs - Specification and Verification of Non-Functional Properties of Program Executions on MPSoCs. In *Proceedings of the 19th ACM-IEEE International Conference on Formal Methods and Models for System Design* (pp. 21–31). Beijing, CN: New York, NY, USA: Association for Computing Machinery.

**MLA:**

Esper, Khalil, Stefan Wildermann, and Jürgen Teich. "Enforcement FSMs - Specification and Verification of Non-Functional Properties of Program Executions on MPSoCs." *Proceedings of the 19th ACM-IEEE International Conference on Formal Methods and Models for System Design (MEMOCODE'21), Beijing* New York, NY, USA: Association for Computing Machinery, 2021. 21–31.

**BibTeX:** Download