| NUMMER: | 150521 |
| KÜRZEL: | FTMC |
| MODULBEAUFTRAGTE:R: | Prof. Dr.-Ing. Dorothea Kolossa |
| DOZENT:IN: | Prof. Dr. Thomas Zeume |
| FAKULTÄT: | Institut für Kommunikationsakustik |
| SPRACHE: | Deutsch |
| SWS: | 2 |
| CREDITS: | 3 |
| ANGEBOTEN IM: | jedes Sommersemester |
VERANSTALTUNGSART
Moodle
PRÜFUNGEN
| FORM: | Seminarbeitrag, studienbegleitend |
| TERMIN: | Siehe Prüfungsamt. |
LERNFORM
Seminar
LERNZIELE
In der Veranstaltung Model Checking haben wir die theoretischen Grundlagen desModel 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