Stud.IP Uni Oldenburg
University of Oldenburg
24.03.2023 17:19:26
inf453 - Combination of Specification Techniques (Complete module description)
Original version English PDF Download
Module label Combination of Specification Techniques
Modulkürzel inf453
Credit points 6.0 KP
Workload 180 h
Institute directory Department of Computing Science
Verwendbarkeit des Moduls
  • Master's Programme Computing Science (Master) > Theoretische Informatik
Zuständige Personen
Olderog, Ernst-Rüdiger (Module responsibility)
Lehrenden, Die im Modul (Prüfungsberechtigt)
Prerequisites
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


Self-competence
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.

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:


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
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
Form of instruction Comment SWS Frequency Workload of compulsory attendance
Lecture 3 WiSe 42
Exercises 1 WiSe 14
Präsenzzeit Modul insgesamt 56 h
Examination Prüfungszeiten Type of examination
Final exam of module
At the end of the lecture period
exercises and oral exam