Modulcode:	Inf-MAES
Englische Bezeichnung:	Modelling and Analyzing Real-Time Systems
Modulverantwortliche(r):	Prof. Dr. Dirk Nowotka
Turnus:	unregelmäßig (SS15)
Präsenzzeiten:	2V 2Ü
ECTS:	5
Workload:	30 Std. Vorlesung, 30 Std. Präsenzübung, 90 Std. Selbststudium
Dauer:	ein Semester
Modulkategorien:	WISSE (BSc Inf) WI (MSc Inf (15)) WI (MEd Inf) WPI (MEd Inf) IG (MSc Inf) IS (MSc Inf)
Lehrsprache:	Deutsch
Voraussetzungen:	Inf-TGI

Kurzfassung:

Zur Analyse von Echtzeitsystemen müssen geeignete Formalismen zur Modellierung solcher Systeme sowie deren Eigenschaften gewählt und entsprechende Analysealgorithmen untersucht werden. In diesem Modul beschäftigen wir uns mit einer anwendungsorientierten Auswahl solcher Formalismen und Algorithmen, insbesondere mit Zeitautomaten und Modelprüfungsverfahren für die Logik TCTL. Mit einer Einführung in das Werkzeug UPPAAL werden Analysen im industriellen Maßstab ermöglicht.

Lernziele:

Nach der erfolgreichen Absolvierung dieses Moduls besitzt der Teilnehmer bzw. die Teilnehmerin ein Verständnis für eine Technik der automatentheoretischen Formalisierung von Echtzeitsystemen, die Formulierung von Systemeigenschaften mittels TCTL, den Modellprüfungsalgorithmus für Zeitautomaten und TCTL und den Einsatz des Werkzeugs UPPAAL bei praktischen Analyseproblemen.

Lehrinhalte:

Modellierung des Zeitbegriffs für die Formalisierung von Echtzeitsystemen, Einführung eines geeigneten Automatenmodells (sog. Zeitautomaten), Modellierung von zeitabhängigen Berechnungen, Einführung einer geeigneten Logik (TCTL) zur Beschreibung von Systemeigenschaften, Betrachtung des Modellprüfungs-Problems, Einführung in das Werkzeug UPPAAL und die beispielhafte Modellierung und Analyse von Echtzeitsystemen mit UPPAAL.

Weitere Voraussetzungen:

Theoretische Grundlagen der Informatik

Prüfungsleistung:

30-minütige mündliche Prüfung

Lehr- und Lernmethoden:

Vorlesung mit Beamer-Folien und Tafel; Präsenzübungen zur Anwendung des Lehrstoffs und Selbstüberprüfung

Verwendbarkeit:

Literatur:

• E. W. Clarke, O. Grumberg, D. A. Peled. Model Checking. MIT Press, 2001. (Kapitel 17)
• R. Alur, C. Courcoubetis, D. Dill. Model-checking in dense real-time. Information and Computation, 104:2-34, 1993.
• R. Alur, D. Dill. A theory of timed automata. Theoretical Computer Science, 126:183-235, 1994.

Verweise:

Kommentar: