VVZ API is not affiliated with ETH Zurich. Data might be outdated or incorrect. Please view the official ETHZ Vorlesungsverzeichnis for binding information.
Kombination von Spezifikationstechniken
Last Updated: 2026-02-05 14:55:12
Objective
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
Content
Die Vorlesung greift einen aktuellen Forschungstrend im Bereich der formalen Methoden auf, die Kombination und Integration verschiedener Spezifikationstechniken. Im Vordergund 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. Abschliessend werden Erweiterungsmöglichkeiten von CSP-OZ zur Spezifikation zeitkritischer Systeme angesprochen. In den Übungen werden die Inhalte der Vorlesung durch Beispiele vertieft.
Resources
Literature
- 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 ). - G. Smith. The Object-Z Specification Language. Kluwer Academic Publisher, 2000. - C.A.R. Hoare. Communicating Sequential Processes. Prentice Hall, 1985. - A.W. Roscoe. The Theory and Practice of Concurrency. Prentice Hall, 1998. - 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. - E.-R. Olderog. Spezifikation von Daten und Prozessen mit Z und CSP. Vorlesungsskript WS 2003/04, Universität Oldenburg, 2004.
General Information
- Language
- German
- Frequency
- Yearly recurring
Examination
- Type
- session examination
- Mode
- oral 30 minutes
Course Components
| Type | Title | Time & Place | Hours |
|---|---|---|---|
| lecture | Kombination von Spezifikationstechniken |
|
2 h weekly |
| exercise | Kombination von Spezifikationstechniken |
|
2 h weekly |