inf453 - Kombination von Spezifikationstechniken (Vollständige Modulbeschreibung)

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 Informatik (Master) > Theoretische Informatik
Zuständige Personen
  • Olderog, Ernst-Rüdiger (Modulverantwortung)
  • Lehrenden, Die im Modul (Prüfungsberechtigt)
Teilnahmevoraussetzungen

- inf400 Theoretische Informatik I
- inf401 Theoretische Informatik II

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

The course addresses a research trend in formal methods, the combination and integration of different specification methods. It focuses on a concrete combination CSP-OZ of the specification techniques CSP (Communicating Sequential Processes) for processes and Z and Object-Z for data, respectively. Reactive systems are described by CSP-OZ. As a preparation, the specification languages Z and CSP are described, followed by the combination CSP-OZ with its process-oriented semantics. The concepts of refinement and inheritance and the possibility of automatic verification of a sublanguage of CSP-OZ with the FDR model checker for CSP will be discussed. Finally, the course explains possibilities of extending CSP-OZ for the specification of time-critical systems.
Topics:

  • specification of complex data and operations in Z, type definition and pattern calculations of Z, data refinement
  • specifications of communicating processes in CSP, operational semantics of CSP, three abstract semantic models for CSP: Trace semantics, failures semantics, failures-divergences semantics, process refinement in the above semantics, FDR model checker for CSP
  • combined specification method CSP-OZ, transformational semantics as CSP-process, theorems of refinements, object-oriented concepts of class and inheritance in CSP-OZ
Literaturempfehlungen

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.
Links
Unterrichtssprache Deutsch
Dauer in Semestern 1 Semester
Angebotsrhythmus Modul unregelmäßig
Aufnahmekapazität Modul unbegrenzt
Lehr-/Lernform V + Ü
Vorkenntnisse - 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.