Worst-case execution time analysis for real-time Java

Abstract

Die Korrektheit eines Echtzeitsystems ist nicht nur von der Programmlogik, sondern auch von zeitlichen Faktoren abhänging. So muss beispielsweise ein periodisch aufgerufener Programmteil rechtzeitig ausgeführt und auf Ereignisse innerhalb einer festgelegten Frist reagiert werden. Um die Einhaltung dieser Anforderungen zu garantieren, ist eine Worst Case Execution-Time (WCET) Analyse notwendig, um festzustellen, wieviel Zeit die Ausführung eines Programmfragments benötigt.<br />Für sicherheitskritische Systeme ist man im Besonderen an der Berechnung einer sicheren oberen Schranke der maximalen Laufzeit interessiert.<br />Diese Diplomarbeit behandelt die Laufzeitanalyse der sequentiellen Programmteile sicherheitskritischer Java Echtzeitanwendungen. In diesem Rahmen wurde eine Applikation zur Laufzeitanalyse für den Java Prozessor JOP entwickelt und zwei unterschiedliche Techniken zur Berechnung der maximalen Laufzeit implementiert. Zum einen die häufig angewandte Technik der impliziten Pfadenumeration (Implicit Path Enumeration Technique (IPET)), welche die Laufzeitberechnung in ein Netzwerkfluss-Problem überführt. Der zweite Ansatz modelliert Programme als ein Netzwerk von timed automata, eine Erweiterung endlicher Automaten um zeitabhängige Systeme zu modellieren. Dabei wird der model checker uppaal verwendet, um im durch die Automaten implizit gegebenen Zustandsraum nach dem Ausführungspfad mit der maximalen Laufzeit zu suchen. Die Berechnung mit Hilfe von uppaal ist zwar teurer, ermöglicht aber im Gegenzug, Abhängigkeiten des Zeitverhaltens vom bisher aufgeführten Pfad zu modellieren, und damit eine genauere Approximation der maximalen Laufzeit zu erhalten. In beiden der oben skizzierten Ansätze wurde JOP's Methoden Cache berücksichtigt, um die Schranke zu verbessern. Da beide Techniken in dem Analysewerkzeug integriert wurden, konnten sie direkt miteinander verglichen werden. In den durchgeführten Experimenten stellte sich der timed automata Ansatz als für kleinere Programme geeignet heraus, wobei allerdings eine hohe Zahl an Schleifeniterationen die Analysezeit signifikant verlängerte. Die IPET Methode wiederum skalierte sehr gut, lieferte aber im Gegenzug etwas schlechtere Ergebnisse mit der von uns verwendeten Cache-Approximation. Für die Berechnung via model checking scheinen noch zahlreiche Optimierungen möglich, um die Analysezeit zu verringern. Außerdem ergeben sich hiermit weitere, neue Anwendungsgebiete, wie etwa modellbasierte Scheduling Analyse, so dass es lohnenswert erscheint, diesen Ansatz auch in Zukunft weiterzuverfolgen.<br />

Real-time systems are applications which have to meet time constraints, ensuring that periodic tasks are scheduled in time, and events are handled within a permitted delay. In order to show that the system behaves correctly, it is necessary to verify that tasks complete within a given time span. Worst Case Execution Time (WCET) analysis, the static prediction of the time needed to execute a task, therefore plays a central role for safety-critical real-time systems.<br />In this thesis, we discuss the WCET analysis of real-time Java applications, and present a tool analyzing tasks executed on the Java Optimized Processor (JOP). JOP is an implementation of the Java Virtual Machine in hardware, and uses a cache fetching all instructions of a method at once, which needs to be taken into account.<br />Two techniques for calculating a WCET bound have been implemented, the Implicit Path Enumeration Technique (IPET), translating the calculation to a maximum cost circulation problem, and a dynamic approach using the timed automata model checker uppaal. The model checking based approach is computationally more expensive, but capable of modeling timings which depend on the execution history, and therefore has the potential to yield more accurate WCET bounds than the static IPET method. JOP's variable block method cache was included in both timing models, reducing the gap between the actual and the calculated WCET. Both approaches have been integrated in the analysis tool, and we are thus able to directly compare analysis times and the quality of the calculated WCET bound. Experimental results indicate that timed automata model checking using uppaal is at least suitable for the analysis of single methods and smaller tasks, although large loop bounds lead to a significant increase of the time needed for the analysis. IPET on the other hand scales very well, but delivered slightly worse results for the cache approximation. As the model checking approach is not established yet, there seem to be plenty of opportunities for optimizations and new applications, leaving room for future research.<br />