Stud.IP Uni Oldenburg
Universität Oldenburg
25.09.2021 06:09:42
inf453 - Kombination von Spezifikationstechniken (Vollständige Modulbeschreibung)
Originalfassung Englisch PDF Download
Modulbezeichnung Kombination von Spezifikationstechniken
Modulkürzel inf453
Kreditpunkte 6.0 KP
Workload 180 h
Einrichtungsverzeichnis Department für Informatik
Verwendbarkeit des Moduls
  • Master Eingebettete Systeme und Mikrorobotik (Master) > Akzentsetzungsmodule
  • Master Informatik (Master) > Theoretische Informatik
Zuständige Personen
Hein, Andreas (Prüfungsberechtigt)
Olderog, Ernst-Rüdiger (Prüfungsberechtigt)
Lehrenden, Die im Modul (Prüfungsberechtigt)
Teilnahmevoraussetzungen
Kompetenzziele
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
Modulinhalte
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
Datenverfeinerung
  • Spezifikation von kommunizierenden Prozessen in CSP, operationelle Semantik von CSP, drei abstrakte
semantische Modelle für CSP: Trace-Semantik, Failures-Semantik, Failures-Divergences-Semantik,
Prozessverfeinerung in diesen Semantiken, FDR Model-Checker für CSP
  • kombinierte Spezifikationsmethode CSP-OZ, transformationelle Semantik als CSP-Prozess,
Sätze über Verfeinerungen, objekt-orientierte Konzepte von Klassen und Vererbung in CSP-OZ
Literaturempfehlungen
Essenziell:

Empfohlen:
  • 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.
Links
Unterrichtssprache Deutsch
Dauer in Semestern 1 Semester
Angebotsrhythmus Modul unregelmäßig
Aufnahmekapazität Modul unbegrenzt
Modullevel / module level BC (Basiscurriculum / Base curriculum)
Modulart / typ of module je nach Studiengang Pflicht oder Wahlpflicht
Lehr-/Lernform / Teaching/Learning method
Vorkenntnisse / Previous knowledge - inf400 Theoretische Informatik I
- inf401 Theoretische Informatik II
Lehrveranstaltungsform Kommentar SWS Angebotsrhythmus Workload Präsenz
Vorlesung
3 WiSe 42
Übung
1 WiSe 14
Präsenzzeit Modul insgesamt 56 h
Prüfung Prüfungszeiten Prüfungsform
Gesamtmodul
Am Ende der Vorlesungszeit
Fachpraktische Übungen und mündliche Prüfung.