622.050 (12W) Specification and Verification

Wintersemester 2012/13

Registration deadline has expired.

First course session
02.10.2012 08:00 - 10:00 On Campus

... no further dates known

Overview

Lecturer

Univ.-Prof. Dipl.-Ing. Dr. Andreas Bollin

Course title german

Spezifikation und Verifikation

Type

Lecture

Hours per Week

2.0

ECTS credits

2.0

Registrations

Organisational unit

Institut für Informatik-Systeme

Language of instruction

German

Course begins on

02.10.2012

Time and place

List of events is loading...

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ädikatenlogik

Literature

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 proofs

Topics

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 calculus

Literature

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.

German
English

Assessment criteria / Standards of assessment for examinations

Online-Klausur (mittels SPU)

Assessment criteria / Standards of assessment for examinations

Written examination with the SPU environment

Grading scheme

Grade / Grade grading scheme

Position 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)

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)

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)

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)

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)

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)

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)

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)

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 2014/15

622.050 VO Spezifikation und Verifikation (2.0h / 2.0ECTS)

Wintersemester 2013/14

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)