Fortgeschrittene Themen des Model Checking

NUMMER: 150521
KÜRZEL: FTMC
MODULBEAUFTRAGTE:R: Prof. Dr. Thomas Zeume
DOZENT:IN: Prof. Dr.-Ing. Dorothea Kolossa
FAKULTÄT: Institut für Kommunikationsakustik
SPRACHE: Deutsch
SWS: 2
CREDITS: 3
WORKLOAD: 90 Stunden
ANGEBOTEN IM: jedes Sommersemester

PRÜFUNGEN

FORM: Seminarbeitrag, studienbegleitend
ANMELDUNG:
DATUM: 0000-00-00
BEGINN: 00:00:00
DAUER:
RAUM:

LERNFORM

Seminar

LERNZIELE

In der Veranstaltung Model Checking haben wir die theoretischen Grundlagen des
Model Checkings kennen gelernt. Insbesondere haben wir die Spezifikationssprachen LTL und
CTL eingefuhrt, ihre Ausdrucksst ¨ ¨arke untersucht, und die wichtigsten algorithmischen Ans¨atze
fur das Model Checking erarbeitet.

INHALT

Wie kann die Korrektheit von Software und Hardware formal überprüft werden? Im ¨
Model Checking werden Software- und Hardware-Module durch Transitionssysteme formalisiert; gewünschte Eigenschaften mit Hilfe logischer Formalismen formal beschrieben; und mit ¨
Hilfe von Algorithmen automatisiert überprüft, ob ein Transitionssystem eine formal spezifizierte Eigenschaft besitzt.
In diesem Seminar wollen wir uns mit weiterführenden, aktuellen Themen im Bereich Model ¨
Checking beschäftigen.

VORAUSSETZUNGEN CREDITS

Keine

EMPFOHLENE VORKENNTNISSE

Veranstaltung “Model Checking”