inf453 - Kombination von Spezifikationstechniken (Vollständige Modulbeschreibung)

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

Der Kurs behandelt einen Forschungstrend in den formalen Methoden, die Kombination und Integration verschiedener Spezifikationsmethoden. Der Schwerpunkt liegt auf einer konkreten Kombination CSP-OZ der Spezifikationstechniken CSP (Communicating Sequential Processes) für Prozesse und Z bzw. Object-Z für Daten. Reaktive Systeme werden durch CSP-OZ beschrieben. Zur Vorbereitung werden die Spezifikationssprachen Z und CSP beschrieben, gefolgt von der Kombination CSP-OZ mit ihrer prozessorientierten Semantik. Die Konzepte der Verfeinerung und Vererbung sowie die Möglichkeit der automatischen Verifikation einer Teilsprache von CSP-OZ mit dem FDR Model Checker für CSP werden diskutiert. Schließlich werden Möglichkeiten der Erweiterung von CSP-OZ für die Spezifikation zeitkritischer Systeme erläutert.
 

Themen:

• Spezifikation von komplexen Daten und Operationen in Z, Typdefinition und Musterberechnungen von Z, Datenverfeinerung
• Spezifikation von kommunizierenden Prozessen in CSP, operationale Semantik von CSP, drei abstrakte semantische Modelle für CSP: Trace-Semantik, Failures-Semantik, Failures-Divergences-Semantik, Prozessverfeinerung in den obigen Semantiken, FDR-Modell-Checker für CSP
• kombinierte Spezifikationsmethode CSP-OZ, transformatorische Semantik als CSP-Prozess, Theoreme der Verfeinerung, objektorientierte Konzepte von Klasse und Vererbung in CSP-OZ

Essential:

• M. Spivey. The Z Notation - A Reference Manual. Prentice Hall, 1989 (siehe http://spivey.oriel.ox.ac.uk/~mike/zrm/index.html).
• Jim Woodcock and Jim Davies. Using Z - Specification, Refinement, and Proof. Prentice Hall, 1996 (siehe http://www.usingz.com).
• A.W. Roscoe. The Theory and Practice of Concurrency. Prentice Hall, 1998.

Recommended:

• C. Fischer. CSP-OZ: A Combination of Object-Z and CSP. In H. Bowmann, J. Derrick (Editors). Formal Methods for Open Object-Based Distributed Systems (Chapman & Hall, 1997) 423-438.
• G. Smith. The Object-Z Specification Language. Kluwer Academic Publisher, 2000.

Am Ende der Vorlesungszeit

Fachpraktische Übungen und mündliche Prüfung.