Kurzportrait

Ein Echtzeitsystem muss korrekte Berechnungen bzw. Reaktionen
innerhalb vorgegebener Zeitschranken zusichern können und damit
Verhersagbarkeit garantieren.
Implemtierungstechnisch besteht ein Echtzeitsystem typischerweise
aus mehreren Prozessen mit unterschiedlicher Priorität. Um
Vorhersagen über die Einhaltung von Zeitschranken machen zu
können, wird jeweils der höchstpriorisierte rechenbereite Prozess
ausgeführt. Bei der Synchronieriung solcher Prozesse tritt das Phänomen der
Prioritätsumkehr auf, indem ein hoch priorisierter Prozess
unbeschränkt lange verzögert werden kann. Verschiedene Protokolle
zur Vermeidung der Prioritätsumkehr wurden daraufhin entwickelt
und stehen auf der Ebene von Betriebssystemen und Laufzeitsystemen
zur Verfügung.
Leider gibt es bei der der Bescheibung der Protokolle Fehler und
Missverständlichkeiten. Darüberhinaus halten sich verschiedene
Implementierungen nur vage an die vorgegebenen Protokolle. Die
Folge davon ist, dass sich die Einhaltung von Zeitschranken nicht
sicher vorsagen lässt.
Aus diesen Gründen wird eine eindeutige Darstellung der Protokolle
entwickelt und die Einhaltung von Zeitschranken
bewiesen. Im nächsten Schritt werden aus dieser Darstellung
Testszenarien abgeleitet, die dazu dienen, Implementierungen
hinsichtlich ihrer Konformität zu der verifizierten Protokollen zu
überprüfen. Bei Defiziten in der Konformität von Implementierungen
ist zu überprüfen, welche Vorhersagen über die Einhaltung von
Zeitschranken noch gemacht werden können.