Formale Spezifikation von Systemen

Protokolle

WS 2004/05

• Gedächtnisprotokoll

Formale Spezifikation von Systemen ist eine Basisveranstaltung im Fachgebiet TFS (Studiengebiet THI) im Informatik-Hauptstudium.

Inhalt

(Von der Website geklaut)

Diese Basis-LV der Theoretischen Informatik führt in die formale Spezifikation von Systemen und damit in grundlegende Probleme und Methoden der theoretischen Informatik ein. Vorrangig werden hierbei Datentyp- und Prozessspezifikation von Softwaresystemen behandelt. Eine durchgänige praxisorientierte Fallstudie aus dem Bereich Logistik dient zur Veranschaulichung und Illustration der vermittelten theoretischen Konzepte.

Im ersten Teil werden zur formalen Modellierung von Prozessen Petrinetze eingeführt, die hier exemplarisch für eine Vielzahl von Prozessmodellierungstechniken vorgestellt werden. Es werden mathematische Methoden sowohl zur Analyse als auch zur Strukturierung und Komposition von Prozessen behandelt. Dabei werden Petrinetze zunächst unabhängig von der Datenmodellierung behandelt.

Zu Beginn des zweiten Teils werden die in TheGI 2 behandelten algebraischen Strukturen kurz wiederholt. Darauf aufbauend werden dann Konzepte der algebraischen Spezifikation von Datentypen aus Sicht von Systemen vorgestellt (Korrektheit, Parameterisierung, First Order Logik - Spezifikation). Bei der algebraischen Spezifikation von nicht parametrisierten Datentypen stehen in dieser Veranstaltung Probleme der Semantik und Korrektheit im Vordergrund, die mit Methoden der Algebra und Logik analysiert werden. Die Parametrisierung von Datentypen ist ein wesentlicher Schritt im Hinblick auf die Modellierung generischer Softwaresysteme und Softwarekomponentenkonzepte.

Für weitergehende Perspektiven wird am Ende der LV ein Ausblick auf die Integration von algebraischen Spezifikationen mit Petrinetzen im Rahmen von algebraischen High-Level Netzen gegeben.

Die in dieser LV erworbenen Kenntnisse sind in vielen anderen Haupstudiums-LV's auch ausserhalb des Studiengebiets THI erfolgreich anwendbar. Sie bilden insbesondere für Schwerpunktsetzungen in den Studiengebieten SSG, PSS, DIS, KI und BKS eine sinnvolle und wichtige Ergänzung.

Tipps und nützliche Infos

Wer mit TheGI2 keine grossen Probleme gehabt hat, ist hier ganz richtig. Die Uebungsblaetter sind nicht so schwer, und Referate (zwei pro Gruppe) muss man frueher oder spaeter sowieso halten. Im zweiten Teil wird der Stoff aus TheGI 2 wiederholt (recht ausfuehrlich) und noch vertieft, man muss sich den Stoff nicht selbst nochmal ansehen. Die Vorlesung ist recht kurzweilig, Prof. Ehrig war wesentlich lockerer, als ich ihn aus meiner TheGI2-Zeit in Erinnerung habe.

Fuer den Petrinetz-Teil gibt es ein Script, das ich aber nur fuer mein Referat benoetigt habe - hier stehen die Beweise ausfuehrlich drin, waehrend sie in der VL eher kurz angesprochen werden. Es gibt eine Buchempfehlung fuer den zweiten Teil, aber da habe ich nicht reingesehen. Teilweise ist auch das TheGI2-Buch noch hilfreich.

Weblinks

• Formale Spezifikation von Systemen (WS2004/2005)
• Formale Spezifikation von Systemen (WS2005/2006)

Persönliche Kommentare

(Nicht unterschriebene Kommentare werden gelöscht!)

Klasse, hat mir viel Spass gemacht! FelixB