Symbolic representations in WCET analysis
Stephan Wilhelm · Publications of the UdS (Saarland University) · 2011
Reliable task-level execution time information is indispensable for validating the correct operation of safety-critical embedded real-time systems. Static worst-case execution time (WCET) analysis is a method that computes safe upper bounds of the execution time of single uninterrupted tasks. The method is based on abstract interpretation and involves abstract hardware models that capture the timing behavior of the processor on which the tasks run. For complex processors, task-level execution time bounds are obtained by a state space exploration which involves the abstract model and the program. Partial state space exploration is not sound. A full exploration can become too expensive. Symbolic state space exploration methods using binary decision diagrams (BDDs) are known to provide efficient means for covering large state spaces. This work presents a symbolic method for the efficient state space exploration of abstract pipeline models in the context of static WCET analysis. The method has been implemented for the Infineon TriCore 1 which is a real-life processor of medium complexity. Experimental results on a set of benchmarks and an automotive industry application demonstrate that the approach improves the scalability of static WCET analysis while maintaining soundness. Zuverlassige Informationen uber die Ausfuhrungszeiten von Programmen sind unerlasslich, um das korrekte Verhalten von sicherheitskritischen eingebetteten Echtzeitsystemen zu garantieren. Die statische Analyse der langsten Ausfuhrungszeit, der sogenannten WCET, ist eine Methode zur Berechnung sicherer oberer Schranken der Ausfuhrungszeiten einzelner, nicht unterbrochener Programmtasks. Sie beruht auf der Methode der Abstrakten Interpretation und verwendet abstrakte Modelle, die das Zeitverhalten des Prozessors erfassen, auf dem die Programme ausgefuhrt werden. Die Berechnung der Ausfuhrungszeitschranken komplexer Prozessoren basiert auf der Exploration eines Zustandsraums, der sowohl das abstrakte Modell, als auch das Programm umfasst. Eine nur teilweise Abdeckung dieses Zustandsraums liefert dabei keine verlasslichen Ergebnisse. Eine vollstandige Exploration ist hingegen sehr aufwandig. Symbolische Methoden, die binare Entscheidungsdiagramme (BDDs) verwenden, sind dafur bekannt, dass sie die effiziente Abdeckung groser Zustandsraume erlauben. Die vorliegende Arbeit stellt eine symbolische Methode zur effizienten Exploration von Zustandsraumen abstrakter Pipelinemodelle im Rahmen der statischen WCET-Analyse vor. Die Methode wurde fur einen realen Prozessor mittlerer Komplexitat, den Infineon TriCore 1, implementiert. Ergebnisse von Experimenten mit Benchmarks sowie mit einer Anwendung aus dem Automobilbereich zeigen, dass der Ansatz die Skalierbarkeit statischer WCET-Analyse verbessert, wobei die Zuverlassigkeit der berechneten Schranken gewahrt bleibt.