Document Open Access Logo

Multi-Requirement Enforcement of Non-Functional Properties on MPSoCs Using Enforcement FSMs - A Case Study

Authors Khalil Esper, Stefan Wildermann, Jürgen Teich

PDF
Thumbnail PDF

File

OASIcs.NG-RES.2022.2.pdf
  • Filesize: 1.05 MB
  • 13 pages

Document Identifiers

Author Details

Khalil Esper
  • Friedrich-Alexander-Universität Erlangen-Nürnberg (FAU), Germany
Stefan Wildermann
  • Friedrich-Alexander-Universität Erlangen-Nürnberg (FAU), Germany
Jürgen Teich
  • Friedrich-Alexander-Universität Erlangen-Nürnberg (FAU), Germany

Funding

This work is funded by the Deutsche Forschungsgemeinschaft (DFG, German ResearchFoundation) – Project Number 146371743 - TRR 89 Invasive Computing.

Cite As Get BibTex

Khalil Esper, Stefan Wildermann, and Jürgen Teich. Multi-Requirement Enforcement of Non-Functional Properties on MPSoCs Using Enforcement FSMs - A Case Study. In Third Workshop on Next Generation Real-Time Embedded Systems (NG-RES 2022). Open Access Series in Informatics (OASIcs), Volume 98, pp. 2:1-2:13, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2022) https://doi.org/10.4230/OASIcs.NG-RES.2022.2

Abstract

Embedded system applications usually have to meet real-time, energy or safety requirements on programs typically concurrently executed on a given MPSoC target platform. Enforcing such properties, e.g., by adapting the number of processors allocated to a program or by scaling the voltage/frequency mode of involved processors, is a difficult problem to solve, especially with a typically large varying environmental input (workload) per execution. In a previous work [Esper et al., 2021], we formalized the related enforcement problem using (a) finite state machines to model enforcement strategies, (b) discrete-time Markov chains to model the uncertain environment determining the system’s workload, and (c) the system response that defines the feedback for the reactive enforcer. In this paper, we apply that approach to specify and verify multi-requirement enforcement strategies and assess a case study for enforcing two independent requirements at the same time, i.e., latency and energy consumption. We evaluate and compare different enforcement strategies using probabilistic verification for the use case of an object detection application.

Subject Classification

ACM Subject Classification
  • Computer systems organization → Multicore architectures
  • Theory of computation → Linear logic
  • Theory of computation → Modal and temporal logics
  • Hardware → Finite state machines
  • Computer systems organization → Self-organizing autonomic computing
  • Theory of computation → Verification by model checking
  • Mathematics of computing → Probabilistic representations
Keywords
  • Runtime Requirement Enforcement
  • Verification
  • Finite State Machine
  • Markov Chain
  • Energy Consumption
  • Probabilistic Model Cheking
  • PCTL
  • MPSoC

Metrics

  • Access Statistics
  • Total Accesses (updated on a weekly basis)
    0
    PDF Downloads
    0
    Metadata Views

References

  1. Christel Baier, Boudewijn R. Haverkort, Holger Hermanns, and Joost-Pieter Katoen. On the Logical Characterisation of Performability Properties. In Automata, Languages and Programming, 27th International Colloquium, ICALP 2000, Geneva, Switzerland, July 9-15, 2000, Proceedings, volume 1853 of Lecture Notes in Computer Science, pages 780-792. Springer, 2000. Google Scholar
  2. Roderick Bloem, Bettina Könighofer, Robert Könighofer, and Chao Wang. Shield synthesis: Runtime Enforcement for Reactive Systems. In Tools and Algorithms for the Construction and Analysis of Systems, volume 9035 of Lecture Notes in Computer Science, pages 533-548. Springer, 2015. Google Scholar
  3. Khalil Esper, Stefan Wildermann, and Jürgen Teich. A Comparative Evaluation of Latency-Aware Energy Optimization Approaches in Many-Core Systems. In Second Workshop on Next Generation Real-Time Embedded Systems, NG-RES@HiPEAC 2021, January 20, 2021, Budapest, Hungary, volume 87 of OASIcs, pages 1:1-1:12. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2021. Google Scholar
  4. Khalil Esper, Stefan Wildermann, and Jürgen Teich. Enforcement FSMs - Specification and Verification of Non-Functional Properties of Program Executions on MPSoCs. In 19th ACM-IEEE International Conference on Formal Methods and Models for System Design (MEMOCODE'21), 2021. Google Scholar
  5. Antonio Filieri, Henry Hoffmann, and Martina Maggio. Automated design of self-adaptive software with control-theoretical formal guarantees. In Proceedings of the 36th International Conference on Software Engineering, pages 299-310, 2014. Google Scholar
  6. Hans Hansson and Bengt Jonsson. A Logic for Reasoning about Time and Reliability. Formal Aspects of Computing, 6(5):512-535, 1994. Google Scholar
  7. Connor Imes, David HK Kim, Martina Maggio, and Henry Hoffmann. POET: a portable approach to minimizing energy under soft real-time constraints. In 21st IEEE Real-Time and Embedded Technology and Applications Symposium, pages 75-86. IEEE Computer Society, 2015. Google Scholar
  8. Marta Z. Kwiatkowska, Gethin Norman, and David Parker. Quantitative analysis with the probabilistic model checker PRISM. Electron. Notes Theor. Comput. Sci., 153(2):5-31, 2006. Google Scholar
  9. Marta Z. Kwiatkowska, Gethin Norman, and David Parker. PRISM 4.0: Verification of Probabilistic Real-Time Systems. In Computer Aided Verification - 23rd International Conference, CAV 2011, Snowbird, UT, USA, July 14-20, 2011. Proceedings, volume 6806 of Lecture Notes in Computer Science, pages 585-591. Springer, 2011. Google Scholar
  10. David G Lowe. Object recognition from local scale-invariant features. In Proceedings of the seventh IEEE international conference on computer vision, volume 2, pages 1150-1157. Ieee, 1999. Google Scholar
  11. Martina Maggio, Alessandro Vittorio Papadopoulos, Antonio Filieri, and Henry Hoffmann. Automated control of multiple software goals using multiple actuators. In Eric Bodden, Wilhelm Schäfer, Arie van Deursen, and Andrea Zisman, editors, Proceedings of the 2017 11th Joint Meeting on Foundations of Software Engineering, ESEC/FSE 2017, Paderborn, Germany, September 4-8, 2017, pages 373-384. ACM, 2017. Google Scholar
  12. Sumit K. Mandal, Ganapati Bhat, Janardhan Rao Doppa, Partha Pratim Pande, and Ümit Y. Ogras. An energy-aware online learning framework for resource management in heterogeneous platforms. ACM Trans. Design Autom. Electr. Syst., 25(3):28:1-28:26, 2020. Google Scholar
  13. Srinivas Pinisetty, Partha S. Roop, Vidula Sawant, and Gerardo Schneider. Security of pacemakers using runtime verification. In 16th ACM/IEEE International Conference on Formal Methods and Models for System Design, MEMOCODE 2018, Beijing, China, October 15-18, 2018, pages 51-61. IEEE, 2018. Google Scholar
  14. Srinivas Pinisetty, Partha S. Roop, Steven Smyth, Nathan Allen, Stavros Tripakis, and Reinhard von Hanxleden. Runtime enforcement of cyber-physical systems. ACM Trans. Embed. Comput. Syst., 16(5s):178:1-178:25, 2017. Google Scholar
  15. Srinivas Pinisetty, Partha S. Roop, Steven Smyth, Stavros Tripakis, and Reinhard von Hanxleden. Runtime enforcement of reactive systems using synchronous enforcers. In Proceedings of the 24th ACM SIGSOFT International SPIN Symposium on Model Checking of Software, Santa Barbara, CA, USA, July 10-14, 2017, pages 80-89. ACM, 2017. Google Scholar
  16. Fred B. Schneider. Enforceable security policies. ACM Transactions on Information and System Security (TISSEC), 3(1):30-50, 2000. Google Scholar
  17. Jürgen Teich, Michael Glaß, Sascha Roloff, Wolfgang Schröder-Preikschat, Gregor Snelting, Andreas Weichslgartner, and Stefan Wildermann. Language and Compilation of Parallel Programs for *-Predictable MPSoC Execution Using Invasive Computing. In 10th IEEE International Symposium on Embedded Multicore/Many-core Systems-on-Chip, MCSOC 2016, Lyon, France, September 21-23, 2016, pages 313-320. IEEE Computer Society, 2016. Google Scholar
  18. Jürgen Teich, Jörg Henkel, Andreas Herkersdorf, Doris Schmitt-Landsiedel, Wolfgang Schröder-Preikschat, and Gregor Snelting. Invasive computing: An overview. In Michael Hübner and Jürgen Becker, editors, Multiprocessor System-on-Chip - Hardware Design and Tool Integration, pages 241-268. Springer, 2011. Google Scholar
  19. Jürgen Teich, Pouya Mahmoody, Behnaz Pourmohseni, Sascha Roloff, Wolfgang Schröder-Preikschat, and Stefan Wildermann. Run-Time Enforcement of Non-functional Program Properties on MPSoCs. In A Journey of Embedded and Cyber-Physical Systems, pages 125-149. Springer, 2021. Google Scholar
  20. Jürgen Teich, Behnaz Pourmohseni, Oliver Keszöcze, Jan Spieck, and Stefan Wildermann. Run-Time Enforcement of Non-Functional Application Requirements in Heterogeneous Many-Core Systems. In 25th Asia and South Pacific Design Automation Conference, ASP-DAC 2020, Beijing, China, January 13-16, 2020, pages 629-636. IEEE, 2020. Google Scholar
Questions / Remarks / Feedback
X

Feedback for Dagstuhl Publishing


Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail
© 2023-2024 Schloss Dagstuhl – LZI GmbH About DROPS Imprint Privacy Contact