622.050 (14W) Specification and Verification
Overview
- Lecturer
- Course title german Spezifikation und Verifikation
- Type Lecture
- Hours per Week 2.0
- ECTS credits 2.0
- Registrations 42
- Organisational unit
- Language of instruction Deutsch
- Course begins on 01.10.2014
Time and place
List of events is loading...
Course Information
Course content
Einführung in das Schreiben von Software-Spezifikationen am Beispiel von Z. Verifikation von Anforderungen und Korrektheitsbeweise.Topics
- Einführung und Motivation
- Logik erster Ordnung
- Modell-basierte Spezifikationssprache Z
- Beweistechniken
- Anwendungsgebiete
Teaching objective
Ziel der Vorlesung (bzw. des PRs) ist es, eine Notation zu erlernen um die Semantik von Systemen zu spezifizieren und in der Lage zu sein prüfbare Spezifikationen zu entwickeln.Prior knowledge expected
Mengentheorie, Aussagen und PrädikatenlogikLiterature
Diller A. : Z - An Introduction to Formal Methods; 2nd ed., Wiley, 1994. Spivey J.M.: The Z Notation: A Reference Manual; 2nd ed., Prentice-Hall International, 1992. Electronic version: http://spivey.oriel.ox.ac.uk/mike/zrm/zrm.pdf Jacky, Jonathan: THE WAY OF Z: Practical Programming with Formal Methods; Cambridge University Press, 1997. Woodcock J., Davis J.: Using Z: Specification, Refinement, and Proof; Prentice Hall International, 1996.Course content
Introduction to software specification and specification methods. Introduction to a model-based specification language (Z). Verification and proofsTopics
- Introduction and Motivation
- First-order logic and set theory
- The Z specification language
- Refinement and proof
- Fields of application
Teaching objective
Learn a notation to rapidly pin down the semantics of (parts of) a system. Provide the capability for developing formally checkable (verifiable) specifications. Understand the key ideas behind software verification.Prior knowledge expected
Set theory, propositional and predicate calculusLiterature
Diller A. : Z - An Introduction to Formal Methods; 2nd ed., Wiley, 1994. Spivey J.M.: The Z Notation: A Reference Manual; 2nd ed., Prentice-Hall International, 1992. Electronic version: http://spivey.oriel.ox.ac.uk/mike/zrm/zrm.pdf Jacky, Jonathan: THE WAY OF Z: Practical Programming with Formal Methods; Cambridge University Press, 1997. Woodcock J., Davis J.: Using Z: Specification, Refinement, and Proof; Prentice Hall International, 1996.Examination information
Im Fall von online durchgeführten Prüfungen sind die Standards zu beachten, die die technischen Geräte der Studierenden erfüllen müssen, um an diesen Prüfungen teilnehmen zu können.
Assessment criteria / Standards of assessment for examinations
Online-Klausur (mittels SPU)
Assessment criteria / Standards of assessment for examinations
Written examination with the SPU environmentGrading scheme
Grade / Grade grading schemePosition in the curriculum
- Teacher training programme Computer Sciences and Computer Sciences Management (Secondary School Teacher Accreditation)
(SKZ: 884, Version: 04W.7)
-
Stage two
-
Subject: Angewandte Informatik (LI 2.3)
(Compulsory subject)
-
Spezifikation und Verifikation (
2.0h VO / 2.0 ECTS)
- 622.050 Specification and Verification (2.0h VO / 2.0 ECTS)
-
Spezifikation und Verifikation (
2.0h VO / 2.0 ECTS)
-
Subject: Angewandte Informatik (LI 2.3)
(Compulsory subject)
-
Stage two
- Bachelor's degree programme Applied Informatics
(SKZ: 511, Version: 12W.1)
-
Subject: Software Development
(Compulsory elective)
-
Spezifikation und Verifikation (
2.0h VO / 2.0 ECTS)
- 622.050 Specification and Verification (2.0h VO / 2.0 ECTS)
-
Spezifikation und Verifikation (
2.0h VO / 2.0 ECTS)
-
Subject: Software Development
(Compulsory elective)
- Bachelorstudium Informatik
(SKZ: 521, Version: 09W.3)
-
Subject: Spezifikation und Verifikation
(Compulsory elective)
-
Spezifikation und Verifikation (
2.0h VO / 2.0 ECTS)
- 622.050 Specification and Verification (2.0h VO / 2.0 ECTS)
-
Spezifikation und Verifikation (
2.0h VO / 2.0 ECTS)
-
Subject: Spezifikation und Verifikation
(Compulsory elective)
- Bachelor's degree programme Informatics
(SKZ: 521, Version: 03W.1)
-
Subject: Spezifikation und Verifikation
(Compulsory subject)
-
Spezifikation und Verifikation (
2.0h VO / 2.0 ECTS)
- 622.050 Specification and Verification (2.0h VO / 2.0 ECTS)
-
Spezifikation und Verifikation (
2.0h VO / 2.0 ECTS)
-
Subject: Spezifikation und Verifikation
(Compulsory subject)
- Master's degree programme Applied Informatics
(SKZ: 911, Version: 13W.1)
-
Subject: Vertiefung Informatik
(Compulsory subject)
-
Spezifikation und Verifikation (
2.0h VO / 2.0 ECTS)
- 622.050 Specification and Verification (2.0h VO / 2.0 ECTS)
-
Spezifikation und Verifikation (
2.0h VO / 2.0 ECTS)
-
Subject: Vertiefung Informatik
(Compulsory subject)
- Masterstudium Informatik
(SKZ: 921, Version: 09W.1)
-
Subject: Spezifikation und Verifikation
(Compulsory subject)
-
Spezifikation und Verifikation (
2.0h VO / 2.0 ECTS)
- 622.050 Specification and Verification (2.0h VO / 2.0 ECTS)
-
Spezifikation und Verifikation (
2.0h VO / 2.0 ECTS)
-
Subject: Spezifikation und Verifikation
(Compulsory subject)
- Master's degree programme Informatics
(SKZ: 921, Version: 03W.1)
-
Subject: Spezifikation und Verifikation
(Compulsory subject)
-
Spezifikation und Verifikation (
2.0h VO / 2.0 ECTS)
- 622.050 Specification and Verification (2.0h VO / 2.0 ECTS)
-
Spezifikation und Verifikation (
2.0h VO / 2.0 ECTS)
-
Subject: Spezifikation und Verifikation
(Compulsory subject)
- Diploma programme Informatics
(SKZ: 880, Version: 02W)
-
Stage two
-
Subject: Angewandte Informatik inkl. Vertiefungsfach
(Compulsory subject)
-
Spezifikation und Verifikation (
2.0h VO / 2.0 ECTS)
- 622.050 Specification and Verification (2.0h VO / 2.0 ECTS)
-
Spezifikation und Verifikation (
2.0h VO / 2.0 ECTS)
-
Subject: Angewandte Informatik inkl. Vertiefungsfach
(Compulsory subject)
-
Stage two
- Diploma programme Informatics
(SKZ: 880, Version: 02W)
-
Stage three
-
Subject: Angewandte Informatik und Vertiefungsfach
(Compulsory subject)
-
Spezifikation und Verifikation (
2.0h VO / 2.0 ECTS)
- 622.050 Specification and Verification (2.0h VO / 2.0 ECTS)
-
Spezifikation und Verifikation (
2.0h VO / 2.0 ECTS)
-
Subject: Angewandte Informatik und Vertiefungsfach
(Compulsory subject)
-
Stage three
Equivalent courses for counting the examination attempts
-
Wintersemester 2023/24
- 622.050 VO Spezifikation und Verifikation (2.0h / 2.0ECTS)
-
Wintersemester 2022/23
- 622.050 VO Spezifikation und Verifikation (2.0h / 2.0ECTS)
-
Wintersemester 2021/22
- 622.050 VO Spezifikation und Verifikation (2.0h / 2.0ECTS)
-
Wintersemester 2020/21
- 622.050 VO Spezifikation und Verifikation (2.0h / 2.0ECTS)
-
Wintersemester 2019/20
- 622.050 VO Spezifikation und Verifikation (2.0h / 2.0ECTS)
-
Wintersemester 2018/19
- 622.050 VO Spezifikation und Verifikation (2.0h / 2.0ECTS)
-
Wintersemester 2017/18
- 622.050 VO Spezifikation und Verifikation (2.0h / 2.0ECTS)
-
Wintersemester 2016/17
- 622.050 VO Spezifikation und Verifikation (2.0h / 2.0ECTS)
-
Wintersemester 2015/16
- 622.050 VO Spezifikation und Verifikation (2.0h / 2.0ECTS)
-
Wintersemester 2013/14
- 622.050 VO Spezifikation und Verifikation (2.0h / 2.0ECTS)
-
Wintersemester 2012/13
- 622.050 VO Spezifikation und Verifikation (2.0h / 2.0ECTS)
-
Wintersemester 2011/12
- 622.050 VO Spezifikation und Verifikation (2.0h / 2.0ECTS)
-
Wintersemester 2010/11
- 622.050 VO Spezifikation und Verifikation (2.0h / 2.0ECTS)
-
Wintersemester 2009/10
- 622.050 VO Spezifikation und Verifikation (2.0h / 2.0ECTS)