Enforcement FSMs - Specification and Verification of Non-Functional Properties of Program Executions on MPSoCs

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

Event location: Beijing CN

ISBN: 9781450391276

DOI: 10.1145/3487212.3487348

Abstract

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.

Authors with CRIS profile

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)

Related research project(s)

Basics of Invasive Computing (A01) (SFB/TRR 89 InvasIC (A01)) DFG SFB/Transregio 89 "Invasive Computing" (TRR 89) July 1, 2010 - Dec. 31, 2022

How to cite

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