Stud.IP Uni Oldenburg
University of Oldenburg
09.12.2021 15:03:13
inf453 - Combination of Specification Techniques (Complete module description)
Original version English Download as PDF
Module label Combination of Specification Techniques
Module code inf453
Credit points 6.0 KP
Workload 180 h
Institute directory Department of Computing Science
Applicability of the module
  • Master's Programme Computing Science (Master) > Theoretische Informatik
  • Master's Programme Embedded Systems and Microrobotics (Master) > Akzentsetzungsmodule
Responsible persons
Hein, Andreas (Authorized examiners)
Olderog, Ernst-Rüdiger (Authorized examiners)
Lehrenden, Die im Modul (Authorized examiners)
inf400/inf401 Theoretische Informatik I and II
Skills to be acquired in this module
Introduction to the specification languages Z for data, CSP for processes, and their combination CSP-OZ for reactive systems with data and process parts.

Professional competence
The students:
  • specify data and processes with Z, CSP and CSP-OZ formally
  • check data refinement relations formally
  • verify CSP-OZ specifications with FDR model checker

Methodological competence
The students:
- are able to integrate complementary specification methods

Social competence
The students:
  • work together in small groups to solve problems
  • present solutions to problems to groups of other students

The students:
  • learn persistence in pursuing difficult tasks 
  • learn precision in specifying problems
Module contents
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.

  • 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
Reader's advisory

  • 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.
Language of instruction German
Duration (semesters) 1 Semester
Module frequency unregelmäßig
Module capacity unlimited
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
Course type Comment SWS Frequency Workload of compulsory attendance
3 WiSe 42
1 WiSe 14
Total time of attendance for the module 56 h
Examination Time of examination Type of examination
Final exam of module
At the end of the lecture period
exercises and oral exam