Stud.IP Uni Oldenburg
University of Oldenburg
15.10.2019 18:48:04
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
Faculty/Institute Department of Computing Science
Used in course of study
  • Master's Programme Computing Science (Master) >
  • Master's Programme Embedded Systems and Microrobotics (Master) >
Contact person
Module responsibility
Authorized examiners
Entry requirements
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
Reader's advisory
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 BC (Basiscurriculum / Base curriculum)
Modulart je nach Studiengang Pflicht oder Wahlpflicht
Lern-/Lehrform / Type of program
Vorkenntnisse / Previous knowledge - inf400 Theoretische Informatik I
- inf401 Theoretische Informatik II
Course type Comment SWS Frequency Workload attendance
Lecture 3.00 WiSe 42 h
Exercises 1.00 WiSe 14 h
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