Struktur und Hierarchie in Echtzeit-Systemen (Structure and Hierarchy in Real-Time Systems) Geschrieben von M. Oliver Möller als Teil der Erforderlichen Leistungen zum Erhalt eines Doktortitels (PhD degree in science). Sprache: Englisch Eingereicht: Aarhus, Dänemark. 20 Februar 2002. Zusammenfassung (Übersetzt). Die Entwicklung digitaler Systeme ist eine besondere Herausforderung, wenn die Korrektheit von einer Zeitkomponente abhängig ist. Ein Ansatz die Zuverlässigkeit solcher Systeme zu erhöhen ist die Modell-basierte Entwicklung. Diese ermöglicht eine formale Analyse über alle Phasen des Entwicklungsprozesses hinweg. Erschwert wird Modell-basierte Entwicklung hauptsächlich durch den Mangel an geeigneten Modellierungssprachen und dem hohen Zeit- und Speicheraufwand einer automatisierten Analyse. In dieser Dissertation verbessern wir die Situation in beiderlei Hinsicht. Erstens bringen wir das mathematische Modell näher an den Entwickler heran. Erreicht wird das durch die Einführung hierarchischer Strukturen -- bekannt aus Statechart-ähnlichen Formalismen -- in ein formales Modell für zeitkritische Systeme. Dies ergibt eine ausdrucksstarke Modellierungssprache, die immer noch eine vollständig automatisierte Analyse des Systems zuläßt. Zweitens verwenden wir zulässige Vergröberungen des Systems, um die Analyse hinsichtlich zeitlicher Eigenschaften effizienter zu gestalten. Wir stellen zwei neue zustandsbasierte Verfahren vor, die Zeit- und Speicherverbrauch bei der automatisierten Analyse drastisch reduzieren können. Das erste Verfahren verwendet strukturelle Informationen, insbesonders Schleifen, um Regelmäßigkeiten im Erreichbaren Zustandsraum ausnützen zu können. Mittels abkürzungsartiger Beifügungen zum Modell kann die Wiederholung ähnlicher zeitversetzter Zustände beim Auffalten des Zustandsraums unterdrückt werden. Das zweite Verfahren wendet das Rahmenwerk der abstrakten Interpretation auf zeitkritische Systeme an. Wir erhalten dabei die Kontrollstruktur eines Systems und abstrahieren lediglich die (teurere) Zeitkomponente eines Zustands. Für die Verifikation unendlichen Verhaltens, auch als "liveness properties" bekannt, ist eine Annahme über das unablässige Fortschreiten von Zeit erforderlich. Wir benützen diese Annahme, um das operationelle Schrittverhalten des Systems mit Hinsicht auf Zeitschritte einzuschränken. Für eine Version des µ-Kalküls, aus welcher der Operator "nächster Zustand" entfernt wurde, ändert diese Einschränkung die Menge der gültigen Formeln nicht. Wir ergänzen unsere Forschungsergebnisse mit experimentellen Laufzeitdaten. Diese sind anhand von prototypischen Implementierungen gemessen, die an die Modelchecker UPPAAL und MOCHA angebunden wurden.