193
Teilnahmepflicht

Wenn eine Veranstaltungsinstanz aus einer Schablone erstellt wird, befindet sie sich in diesem Zustand.

  • Die Daten sind in der Regel noch nicht vollständig und es kann noch alles bearbeitet werden.
  • Dozenten und Sekretariate können den Zuständ auf Bearbeitet setzen.

  • Unterschied zwischen Programmieren und Modellieren
  • Modellieren reaktiver Systeme in SPIN und Promela
  • Spezifizieren von Anforderungen in temporalen Logiken
  • Automatentheoretische Modelle von Systemen und Spezifikationen
  • Entscheidungsverfahren für temporale Logiken
  • Symbolisches Modelchecking und Binäre Entscheidungsdiagramme
  • Modelchecking mit NuSMV
  • Automatenmodelle mit Zeit
  • Modellchecking von Zeitautomaten mit Uppaal
  • Formale Methoden zur Abstraktion und dem Nachweis der erhaltenen Eigenschaften.

Sprachübergreifend

193 041
Teilnahmepflicht

193 041
Teilnahmepflicht

Werdende Mütter

Keine Gefährdungen vorliegend
Teilweise Gefährdungen vorliegend
Alternative Lehrveranstaltung
Gefährdungen vorliegend

Stillende Mütter

Keine Gefährdungen vorliegend
Teilweise Gefährdungen vorliegend
Alternative Lehrveranstaltung
Gefährdungen vorliegend

Begleitveranstaltungen

Übung zu Modelchecking

Werdende Mütter

Keine Gefährdungen vorliegend
Teilweise Gefährdungen vorliegend
Alternative Lehrveranstaltung
Gefährdungen vorliegend

Stillende Mütter

Keine Gefährdungen vorliegend
Teilweise Gefährdungen vorliegend
Alternative Lehrveranstaltung
Gefährdungen vorliegend

Projektseminar zu Modelchecking

Werdende Mütter

Keine Gefährdungen vorliegend
Teilweise Gefährdungen vorliegend
Alternative Lehrveranstaltung
Gefährdungen vorliegend

Stillende Mütter

Keine Gefährdungen vorliegend
Teilweise Gefährdungen vorliegend
Alternative Lehrveranstaltung
Gefährdungen vorliegend