Kolloquium Prof. Dr. Dr. h.c. R. Wilhelm

Am Freitag, 26. Oktober 2018, um 14:00 Uhr, im Raum N 1058 des Informatikgebäudes wird Herr Prof. Dr. Dr. h.c. Reinhard Wilhelm der Universität des Saarlandes einen Vortrag zum Thema: Timing Verification of Real-Time Systems halten. Der Lehrstuhl für Systemnahe Informatik am Institut für Informatik lädt hierzu herzlich ein. Eine Anmeldung ist nicht erforderlich.
Titel: Timing Verification of Real-Time Systems
Termin: 26.10.2018, 14:00 Uhr
Gebäude/Raum: N 1058
Ansprechpartner: Prof. Dr. Ungerer


Hard real-time systems are subject to stringent timing constraints which are dictated by the surrounding physical environment. A schedulability analysis has to be performed in order to guarantee that the timing constraints of all co-executed tasks on a given platform will be met ("timing validation"). Schedulability analysis requires upper bounds for the execution times of all the system's tasks to be known. These upper bounds are commonly called worst-case execution times (WCETs). The WCET-determination problem has become non-trivial due to the advent of processor features such as caches, pipelines, and all kinds of speculation, which make the execution time of an individual instruction dependent on the execution state, e.g. the contents of the caches. Such execution times may vary between a few cycles and several hundred cycles. A combination of Abstract Interpretation (AI) with Integer Linear Programming (ILP) has been successfully used to determine precise upper bounds on the execution times of real-time programs. The task solved by abstract interpretation is to compute invariants about the processor's execution states at all program points. These invariants describe the contents of caches, of the pipeline, of prediction units etc. They allow to verify local safety properties, safety properties that correspond to the absence of "timing accidents". Timing accidents, e.g. cache misses, pipeline stalls are reasons for the increase of the execution time of an individual instruction in an execution state. The technology and tools have been used in the certification of several time-critical subsystems of the Airbus A380, the Airbus A350, and the M400. The tool aiT, developed by our spin-off company AbsInt, is the only tool worldwide, validated for these avionics applications.