Veranstaltungsarten (SWS)
Vorlesung: 2 │ Übung: 2 │ Praktikum: 0 │ Seminar: 0
Prüfungsnummer: ZKD 59001
Lehrform: Vorlesung und Übung in deutscher Sprache an der Tafel; englisches Arbeitsmaterial
Sprache: Deutsch
Turnus: WS
ECTS: 6
Prüfungsleistung Klausur (90 min.)
Mündliche Prüfung (30-45 min.)
zugeordnete Studiengänge
zugeordnete Personen
zugeordnete Module
Informationen
Beschreibung: Wie empirische Untersuchungen ergeben haben, scheitern Softwareprojekte oftmals wegen unklarer Anforderungen. Softwaresysteme sollten daher genau spezifiziert werden, bevor mit der Implementierung begonnen wird. Da die natürliche Sprache zu unpräzise für eine genaue Spezifikation ist, sollten formale Sprachen zur Softwarespezifikation verwendet werden. Diese ermöglichen es auch, die Eigenschaften des Softwaresystems zu analysieren, bevor es implementiert ist.

In der Veranstaltung wird die Spezifikationssprache Z gelernt.

Inhalte im Einzelnen:
- Motivation: wozu formale Spezifikation?
- verschiedene Arten formaler Spezifikationssprachen
(daten- vs. verhaltensorientiert, algebraisch- vs. modellbasiert)
- Notation für Mengen und Prädikate
- Z-Methodik
- Object-Z
- Typchecker für Z
Lernziele: - Vor- und Nachteile formaler Spezifikationen nennen können
- Verschiedene Arten formaler Spezifikationssprachen aufzählen und deren Unterschiede erläutern können
- Formale Spezifikationen in Z und Object-Z lesen und interpretieren können
- Formale Spezifikationen in Z und Object-Z anfertigen können
- Den Begriff der Verfeinerung erläutern können
- Verfeinerungsbeweise führen können
- Typchecker anwenden können
Literatur: - J. M. Spivey: The Z Notation - A Reference Manual, Prentice Hall, 1992, verfügbar unter http://spivey.oriel.ox.ac.uk/~mike/zrm/
- J. B. Wordsworth: Software Development with Z, Addison-Wesley, 1992
- G. Smith: The Object-Z Specification Language, Kluwer Academic Publishers, 1999
Vorleistung: Kenntnisse der Softwaretechnik
Infolink:
Bemerkung:
Description: As empirical studies show, software projects often fail because of unclear requirements. Software systems should therefore be precisely specified, before the implementation begins. Since natural language is too imprecise for a detailed specification, formal specification languages should be used. Using such languages enables a developer to analyze the properties of a software system before it is implemented.

In this course, students learn the specification language Z.

Contents in detail:
- Motivation: why formal specification?
- Different types of formal specification languages
(data- vs. behavior-oriented, abgebraic- vs. model-based)
- Notation for sets and predicates
- Z-Methodology
- Object-Z
- Type checker for Z
Learning Targets: - Be able to state state advantages and disadvantages of formal specifications
- Be able to name various types of formal specification languages and explain their differences
- Be able to read and interpret formal specifications in Z and Object-Z
- Be able to develop formal specifications in Z and Object-Z
- Be able to explain the notion of refinement
- Be able to perform refinement proofs
- Be able to use typcheckers
Literature: - J. M. Spivey: The Z Notation - A Reference Manual, Prentice Hall, 1992, verfügbar unter http://spivey.oriel.ox.ac.uk/~mike/zrm/
- J. B. Wordsworth: Software Development with Z, Addison-Wesley, 1992
- G. Smith: The Object-Z Specification Language, Kluwer Academic Publishers, 1999
Pre-Qualifications:
Info Link:
Notice: