inf453 - Combination of Specification Techniques
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 |
|
Zuständige Personen |
|
Prerequisites | |
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.
Methodological competence
Social competence
Self-competence
|
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.
|
Literaturempfehlungen | Essential:
Recommended:
|
Links | |
Language of instruction | German |
Duration (semesters) | 1 Semester |
Module frequency | irregular |
Module capacity | unlimited |
Teaching/Learning method | V + Ü |
Lehrveranstaltungsform | 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 |