Historische Entwicklung

Ausgangspunkt ist das Problem, dass die Ingenieure eines RT-Systems eine Garantie für das System geben müssen, dass es für alle vorgesehenen Ereignisse einer bestimmten Anwendungssituation ein definiertes Verhalten innerhalb vorgegebener Deadlines zeigen soll. Das 'übliche' Verfahren besteht darin, für bestimmte Prioritätsregeln (z.B. Rate Monotonic (RM), Deadline Monotonic (DM), Earliest-Deadline-First (EDF), usw.) sowie einem definierten Schedulingalgorithmus zu beweisen, dass ein optimaler Ablauf garantiert wird, sofern es überhaupt eine Lösung gibt. Dazu muss gezeigt werden, dass für ein hinreichend langes Zeitfenster keine Deadlines gebrochen werden. Dies ist die 'klassische' Methode.

Unabhängig von der Theorie der Realzeitsysteme gibt es seit den 80iger Jahren eine Entwicklung im Bereich des formalen Spezifizierens und automatischen Beweisens, die unter dem Begriff des modellbasierten automatischen Beweisens langsam Eingang findet in immer mehr unterschiedliche Bereiche, auch in den Bereich der RTS-Theorie (für eine ausführlichere Darstellung siehe die Einleitung zu meinem Skript [22]).