Formale Grundlagen der Informatik II (FGI 2):
Modellierung und Analyse von Informatiksystemen
(Wintersemester 2015/16)
Veranstalter:
Daniel Moldt und
Lawrence Cabac
Termin / Ort:
Di. 12:15-13:45 und Do. 12:15-13:45
in (Erzwiss H)
Ort ab 20.10.2015: Stellingen B-201
[Übungen],
[Übungsschein],
[Klausurtermine],
[Diplomstudiengang],
[Materialien] und
[Übungsaufgaben]
[Ressourcen]
Diese Lehrveranstaltung verzahnt in besonderer Weise
die Inhalte der theoretischen Informatik mit denen der
praktischen Informatik - insbesondere solche, die sich
mit verteilter Software befassen.
Behandelt werden u.a. temporale Logik zur Analyse von verteilten Systemen
sowie Petrinetze und Prozessalgebra als Spezifikationsformalismen.
Weitere Details sind im Kommentierten Vorlesungsverzeichnis in Stine zu finden.
Eine Anmeldung in Stine ist Voraussetzung für die Teilnahme.
Die Übungen beginnen am Montag, den 12. Okt. 2015.
(Ja, noch vor der Vorlesung!)
Der aktuelle Plan für die Übungsgruppen
-
G01: Mo. 10-12 in G-203
G02: Mo. 10-12 in C-221
G03: Mo. 10-12 in G-210
-
G04: Mo. 12-14 in G-102
G05: Mo. 12-14 in G-203
-
G06: Mo. 14-16 in G-203
G07: Mo. 14-16 in C-221
-
G08: Di. 10:00 - 11:30 in C-221
G09: Di. 10:00 - 11:30 in G-203
-
Jede Woche wird ein neuer Aufgabenzettel gestellt.
-
Die Lösungen werden in der jeweils darauffolgenden Woche in der Übungsgruppe abgegeben.
-
Die Lösungen werden von den
Übungsgruppenleitern bis zur darauffolgenden Woche korrigiert.
-
Es wird 13 Aufgabenzettel geben, davon 12 mit Hausaufgaben.
Die Aufgaben auf dem 12. Aufgabenzettel sind optional.
Der letzte Aufgabenzettel enthält nur Präsenzaufgaben.
Der erste Aufgabenzettel ist nicht optional.
-
Die Aufgaben sollten in Arbeitsgruppen bearbeitet werden.
Eine Arbeitsgruppe soll aus zwei bis maximal drei Studierenden bestehen.
Arbeitsgruppen geben nur einen Lösungszettel ab, auf dem alle Namen der Teilnehmer(innen) und die Gruppennummer
lesbar notiert sein müssen.
Für die Bescheinigung einer erfolgreichen Teilnahme/Klausurzulassung gilt:
-
Bei allen Übungsterminen gilt Anwesenheitspflicht.
Bei mehr als zweimaligem Fehlen wird eine schriftliche Begründung,
z.B. Attest eines Arztes, benötigt.
-
Eine aktive Teilnahme mit dem Bemühen um konstruktive Beiträge muss gegeben sein.
-
Bei mindestens 2 Aufgabenzetteln muss im Laufe des Semesters eine der Präsenzaufgaben
abschließend vollständig vorgestellt werden.
-
Jedes Arbeitsgruppenmitglied muss die erarbeiteten Lösungen selbst präsentieren.
Dies erfordert eine entsprechende eigenständige Vorbereitung der Präsenzaufgaben.
-
Insgesamt müssen 50 Prozent der Gesamtpunktzahl und mindestens 20 Prozent auf mindestens 10 Aufgabenblättern erreicht werden.
-
Für die FGI-2 Vorlesung wird ein
Olat-Kurs
bereitgestellt.
Dort werden für jede Woche Materialien hinterlegt, die für die jeweilige Woche zu bearbeiten sind.
Für die jeweilige Woche (Ausnahme: erste Woche, die ist optional) ist VOR der ersten Vorlesung der Woche am Dienstag
der Olat-Test mit mind. 60% der Punkte zu bestehen.
Insgesamt müssen 11 der Tests mit mindestens 60% der Punkte bestanden werden.
Ansonsten müssen in den Übungsaufgaben mehr Punkte erreicht werden.
Details dazu gibt es in der ersten Übungsgruppe.
Sämtliche Fragen lassen sich mit Hilfe des Lesestoffes beantworten.
-
Das Kopieren fremder Lösungen führt zu Punktabzügen bei
allen Beteiligten und gilt als Täuschungsversuch.
-
Diplomstudierende können dieses Modul (Vorlesung+ Übung) als
Substitut der Hauptstudiumsgrundlagenvorlesung "Prozesse und Nebenläufigkeit" (PNL) wählen.
Es ist dann auch die FGI-2 Klausur mitzuschreiben.
Alternativ werden weiterhin noch mündliche Prüfung über den
PNL-Stoff dieser Vorlesung angeboten.
-
Diplomstudierende der Wirtschaftsinformatik können Teile dieser Vorlesung als äquivalent zur Vorlesung F4 wählen.
Das Skript wird in den Übungsgruppen in gedruckter Form zum Kauf angeboten.
Interessierte müssen am ersten Termin verbindlich eine Abnahme zusagen.
Der Selbstkostenbeitrag ist zum zweiten Termin mitzubringen.
Weitere Informationen zum Kauf gibt es in den Übungsgruppen.
Benutzername und Passwort für die kostenfreie pdf-Version werden in den Übungen bekanntgegeben.
Vorlesungsfolien können vorab unter den FGI-2 Veranstaltungen der vergangenen Semester eingesehen werden.
Zugangsdaten gibt es bei den Übungsgruppenleitern und Veranstaltern.
Die Vorlesungsfolien:
werden hier fortlaufend hinterlegt.
Folien zu Automaten (13.10.2015)
Folien zu Büchi Automaten und Transitionssysteme (15.10.2015 20.10.2015)
Folien zu Synchrone Produkte von Trasitionssystemen (20.10.2015)
Folien zu Kripkestrukturen (22.10.2015)
Folien zu LTL (27.10.2015 4.11.2015)
Folien zu CTL (4.11.2015)
Folien zu Partial Order und Zeitstempeln
Folien zu Petrinetzen: Einführung
Folien zu Petrinetzen: Prozesse
Folien zur Wiederholung von Petrinetzen: Prozesse
Folien zu Petrinetzen: P/T-Netze und elementare Eigenschaften (erster Teil)
Folien zur Wiederholung von Petrinetzen: P/T-Netze und elementare Eigenschaften
Folien zu Petrinetzen: P/T-Netze und elementare Eigenschaften /zweiter Teil)
Folien zu Verifikation von Petrinetzen: Erreichbarkeit bis Überdeckungsgraph
Folien Woche 07 zweiter Teil: Fairness, Zustandsraumexplosion, Erreichbarkeit,
Überdeckbarkeit, Invarianzeigenschaften, Strenge Zusammenhangskomponenten
Kantenkonstante Netze (KKN) und Gefärbte Netze (CPN) (08.12.2015)
Workflow Netze (WF) (10.12.2015)
Die Aufgaben und das Skript werden im
Olat-System hinterlegt. Direkt zum
FGI2-15/16 in Olat.
Benötigte
Ressourcen für die Übungsaufgaben.