inf453 - Combination of Specification Techniques (Complete module description)

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) >
Zuständige Personen
  • Olderog, Ernst-Rüdiger (module responsibility)
  • Lehrenden, Die im Modul (Prüfungsberechtigt)
Prerequisites

- inf400 Theoretical Computer Science I
- inf401 Theoretical Computer Science 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:

  • 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
Language of instruction German
Duration (semesters) 1 Semester
Module frequency irregular
Module capacity unlimited
Teaching/Learning method V + Ü
Previous knowledge - inf400 Theoretical Computer Science I
- inf401 Theoretical Computer Science 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