Logisch-algebraischer Systementwurf

(LAS)
  • Vertiefungsmodul INF-MSc-318 im SoSe 2020
  • 4 SWS - 6 Credits
  • Vertiefungsmodul in den Masterstudiengängen Informatik und Angewandte Informatik
    Forschungsbereich Software, Sicherheit und Verifikation
  • Dozent und Übungsleiter: Prof. Dr. Peter Padawitz
  • Termine: Mo+Do 14:15-15:45 im OH 12, Raum 3.031
  • Beginn: 20. 4. 2020
  • Bitte UNBEDINGT bei Moodle unter LAS SoSe 2020 einschreiben, da zumindest die ersten Termine aus bekanntem Grund als Videokonferenzen stattfinden und dementsprechend alle Details zu dieser LV online kommuniziert werden!
  • Inhalt: Die LV behandelt die grundlegenden Konzepte zu Konstruktion, Ausführung und Verifikation formaler Modelle. 40 Jahre Forschung und Entwicklung an der Schnittstelle zwischen Mathematik und Softwaretechnik haben zu der heutigen Sicht geführt, nach der jedes Modell konstruktor- oder destruktorbasiert, d.h. über den Aufbau oder das Verhalten seiner Objekte definiert ist. Zur ersten Gruppe von Modellen gehören all diejenigen, die grammatikbasiert oder in anderer Weise induktiv beschrieben werden. Die zweite Gruppe umfasst Automaten, Kripke-Strukturen, Petri-Netze, Berechnungssequenzen, Flussgraphen, Prozessalgebren, Klassenhierarchien, kurzum alle durch Zustandsübergänge und Attribute charakterisierten - oft coinduktiv genannte - Strukturen. Theoretische Untersuchungen und praktische Anwendungen haben gezeigt, dass zwischen induktiven Modellen einerseits und coinduktiven andererseits eine Dualität besteht, die von der Datenstrukturierung bis zu den Rechen- und Beweismethoden reicht.
    Ausgehend von mengentheoretischen Typkonstruktoren wie Produkt, Summe und Quotient werden die zentralen Konzepte der Kategorientheorie (Kategorie, Funktor, natürliche Transformation, Limes, Colimes, F-Algebra, F-Coalgebra, Adjunktion, Monade, Comonade) behandelt. Der Fokus liegt dann auf Kategorien mehrsortiger Mengen bzw. CPOs (Mengen mit kettenvollständiger Halbordnung), welche die semantische Grundlage für funktionallogischer Spezifikationen induktiver wie auch coinduktiver Modelle bilden. Dabei stehen neben der präzisen Beschreibung des jeweiligen Modells die Methoden seiner Ausführung wie der Auswertung von Ausdrücken, der Lösung von Gleichungen und der logischen Ableitung von Eigenschaften im Vordergrund. All diese Prozesse basieren auf Regelsystemen, die zum großen Teil in dem interaktiven Präsentations- und Verifikationswerkzeug Expander2 implementiert sind, das ggf. in der LV eingesetzt wird.
  • Kompetenzen: Die Studierenden lernen einzuschätzen, welche mathematischen Konstruktionen und darauf aufbauenden Methoden für welche Anwendungen mehr oder weniger geeignet sind und wie sie an spezielle Anforderungen anzupassen sind. Eignung entsteht nicht nur durch eine adäquate, präzise Syntax und Semantik, sondern auch durch den Einsatz von Methoden, die nachvollziehbares und möglichst effizientes Rechnen, Lösen und Beweisen in den jeweiligen Modellen ermöglichen. Da Logik und Algebra nicht nur den klarsten begrifflichen Rahmen, sondern auch die mächtigsten und flexibelsten Verfahren bieten, um Softwarespezifikationen zu erstellen und zu analysieren, ist der hinreichend souveräne Umgang mit logisch-algebraischen Techniken ein vordringliches Lernziel.
  • Materialien