Einführung in die Spezifikationssprachen Z für Daten, CSP für Prozesse und deren Kombination CSP-OZ für reaktive Systeme mit Daten- und Prozessanteilen.

Fachkompetenzen
Die Studierenden:

• spezifizieren Daten und Prozesse mit Z, CSP und CSP-OZ formal
• überprüfen Datenverfeinerungsbeziehungen formal
• verifizieren CSP-OZ Spezifikationen mit dem FDR Model-Checker

Methodenkompetenzen
Die Studierenden:

• erwerben die Fähigkeit, komplementäre Spezifikationsmethoden zu integrieren

Sozialkompetenzen
Die Studierenden:

• arbeiten in kleinen Gruppen an Lösungen von Aufgaben
• präsentieren Lösungen von Aufgaben vor Gruppen

Selbstkompetenzen
Die Studierenden:

• erlernen Ausdauer bei der Bearbeitung schwieriger Aufgaben
• erlernen Präzision bei der Spezifikation von Problemen

Die Vorlesung greift einen Forschungstrend im Bereich der formalen Methoden auf, die Kombination und Integration verschiedener Spezifikationstechniken. Im Vordergrund steht eine konkrete Kombination CSP-OZ der Spezifikationstechniken CSP (Communicating Sequential Processes) für Prozesse und Z bzw. Object-Z für Daten. CSP-OZ ist zur Beschreibung von reaktiven Systemen gedacht.

Zur Vorbereitung werden zunächst die Spezifikationssprachen Z und CSP erklärt. Dann wird die Kombination CSP-OZ mit ihrer prozessorientierten Semantik eingeführt. Es werden die Konzepte der Verfeinerung und Vererbung sowie die Möglichkeit einer automatischen Verifikation einer Teilsprache von CSP-OZ mit dem FDR Model-Checker für CSP diskutiert. Abschließend werden Erweiterungsmöglichkeiten von CSP-OZ zur Spezifikation zeitkritischer Systeme angesprochen.

Themen:

• Spezifikation von komplexen Daten und Operationen in Z, Typdefinitionen und Schemakalkül von Z

• Spezifikation von kommunizierenden Prozessen in CSP, operationelle Semantik von CSP, drei abstrakte

• kombinierte Spezifikationsmethode CSP-OZ, transformationelle Semantik als CSP-Prozess,

Am Ende der Vorlesungszeit

Fachpraktische Übungen und mündliche Prüfung.