Eine kompositionelle Performanzanalyse für eingebettete Rechensysteme mit schwach harten Echtzeitanforderungen

This dissertation addresses the problems in several ways: The classical Liu-Layland system model, which is adequate for classic real-time systems, is replaced by a fully curve-based model. The new model specifies both event occurrence and execution time demand by curves; comparable state-of-the-art models apply either event arrival curves or workload curves. Curves significantly better capture variable event arrival and variable execution time demand than single-value parameters as in the Liu-Layland model. The existing timing analysis framework Compositional Performance Analysis (CPA) is adapted in this dissertation such that it processes the fully curve-based model and produces tighter results for timing-related system properties. Apart from the system model, it has also been useful to question the type of real-time constraints that should apply to systems, which by their construction inevitably produce deadline misses in rare cases unless the system is unrealistically lightly loaded. Interestingly, it has been observed in related work that rarely occurring deadline misses can be acceptable for systems which have an inherently robust behavior or appropriate mitigation mechanisms. This has led to the relatively new theory of weakly-hard real-time systems. A weakly-hard real-time system satisfies its timing-related constraints if a maximum number of deadline misses in a given execution window will never be exceeded. This type of real-time constraints is promising because it reconciles the need for formal performance guarantees with the tolerance of occasional deadline misses. Therefore, a compositional analysis framework is developed in this dissertation which is able to formally verify weakly-hard real-time properties of modern embedded systems with a fully curve-based system model. It relies on results from CPA and Typical Worst-Case Analysis (TWCA) and is thus called TypicalCPA. The analysis goes beyond the state-of-the-art in various aspects, but notably it is applicable to heterogeneous multi-component computing platforms where prior methods could only analyze single-component systems with weakly-hard constraints. In the experiments, the method is applied to different synthetically generated systems to evaluate achievable weakly-hard real-time guarantees and related run times. The dissertation can be seen as a comprehensive study how to tackle the challenge of verifying modern embedded computing systems in the future.Diese Dissertation adressiert die Problematik auf verschiedene Weise: Das klassische Liu-Layland-Systemmodell, das für klassische Echtzeitsysteme ausreichend ist, wird durch ein vollständig kurvenbasiertes Modell ersetzt. Das neue Modell spezifiziert sowohl das Auftreten von Ereignissen als auch die Arbeitslast durch sog. Kurven; vergleichbare State-of-the-Art-Modelle verwenden entweder Ereigniskurven oder Lastkurven. Kurven erfassen variierende Ereignisankünfte und variierende Lastzustände wesentlich besser als simple Parameter wie im Liu-Layland-Modell. Das bestehende Timing-Analyse-Framework Compositional Performance Analysis (CPA) wird in dieser Dissertation so angepasst, dass es das vollständig kurvenbasierte Modell verarbeitet und damit dann zeitbezogene Systemeigenschaften genauer berechnet. Abgesehen vom Systemmodell war es auch nützlich, die Art der Echtzeitbeschränkungen zu hinterfragen, die für Systeme gelten sollen, die durch ihre Konstruktion die Überschreitung von Deadlines in seltenen Fällen verursachen, wenn das System nicht gerade unrealistisch wenig ausgelastet ist. Interessanterweise wurde in verwandten Arbeiten beobachtet, dass selten auftretende Deadline-Überschreitungen für Systeme, die ein inhärent robustes Verhalten oder geeignete Toleranzmechanismen aufweisen, akzeptabel sein können. Dies hat zu der relativ neuen Theorie der schwach harten Echtzeitsysteme geführt. Ein schwach hartes Echtzeitsystem erfüllt seine zeitliche Spezifikation, wenn eine maximale Anzahl von Überschreitungen einer Deadline in einem bestimmten Ausführungsfenster nie überschritten wird. Diese Art von Echtzeitspezifikation ist vielversprechend, weil sie den Bedarf an einer formalen Garantie für das Zeitverhalten mit der Toleranz gelegentlicher Deadline-Überschreitungen in Einklang bringt. Daher wird in dieser Dissertation ein kompositionelles Analyseframework entwickelt, das in der Lage ist, schwach harte Echtzeiteigenschaften moderner eingebetteter Systeme mit einem vollständig kurvenbasierten Systemmodell formal zu verifizieren. Das Framework stützt sich auf die Ergebnisse der CPA und der Typical Worst-Case Analysis (TWCA) und wird daher TypicalCPA genannt. TypicalCPA geht in verschiedenen Aspekten über den Stand der Technik hinaus, vor allem aber ist sie auf heterogene Multikomponenten-Rechenplattformen anwendbar, während frühere Methoden nur Einkomponentensysteme mit schwach harten Randbedingungen analysieren konnten. In den Experimenten wird die Methode auf verschiedene synthetisch erzeugte Systeme angewandt, um die erreichbaren schwach harten Echtzeitgarantien und die damit verbundenen Laufzeiten zu bewerten. Die Dissertation kann als eine umfassende Studie gesehen werden wie die formale Verifikation moderner eingebetteter Computersysteme zukünftig realisiert werden kann