622.050 (12W) Spezifikation und Verifikation

Wintersemester 2012/13

Anmeldefrist abgelaufen.

Erster Termin der LV
02.10.2012 08:00 - 10:00 On Campus

... keine weiteren Termine bekannt

Überblick

Lehrende/r

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

LV-Titel englisch

Specification and Verification

LV-Art

Vorlesung

Semesterstunde/n

2.0

ECTS-Anrechnungspunkte

2.0

Anmeldungen

Organisationseinheit

Institut für Informatik-Systeme

Unterrichtssprache

Deutsch

LV-Beginn

02.10.2012

Zeit und Ort

Liste der Termine wird geladen...

Inhalt/e

Einführung in das Schreiben von Software-Spezifikationen am Beispiel von Z. Verifikation von Anforderungen und Korrektheitsbeweise.

Themen

Einführung und Motivation
Logik erster Ordnung
Modell-basierte Spezifikationssprache Z
Beweistechniken
Anwendungsgebiete

Lehrziel

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.

Erwartete Vorkenntnisse

Mengentheorie, Aussagen und Prädikatenlogik

Literatur

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.

Inhalt/e

Introduction to software specification and specification methods. Introduction to a model-based specification language (Z). Verification and proofs

Themen

Introduction and Motivation
First-order logic and set theory
The Z specification language
Refinement and proof
Fields of application

Lehrziel

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.

Erwartete Vorkenntnisse

Set theory, propositional and predicate calculus

Literatur

Prüfungsinformationen

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.

Deutsch
Englisch

Beurteilungskriterien/-maßstäbe

Online-Klausur (mittels SPU)

Beurteilungskriterien/-maßstäbe

Written examination with the SPU environment

Beurteilungsschema

Note Benotungsschema

Position im Curriculum

Diplom-Lehramtsstudium Unterrichtsfach Informatik und Informatikmanagement (SKZ: 884, Version: 04W.7)
- 2.Abschnitt
  - Fach: Angewandte Informatik (LI 2.3) (Pflichtfach)
    - Spezifikation und Verifikation ( 2.0h VO / 2.0 ECTS)
      - 622.050 Spezifikation und Verifikation (2.0h VO / 2.0 ECTS)

Bachelorstudium Angewandte Informatik (SKZ: 511, Version: 12W.1)
- Fach: Softwareentwicklung (Wahlfach)
  - Spezifikation und Verifikation ( 2.0h VO / 2.0 ECTS)
    - 622.050 Spezifikation und Verifikation (2.0h VO / 2.0 ECTS)

Bachelorstudium Informatik (SKZ: 521, Version: 09W.3)
- Fach: Spezifikation und Verifikation (Wahlfach)
  - Spezifikation und Verifikation ( 2.0h VO / 2.0 ECTS)
    - 622.050 Spezifikation und Verifikation (2.0h VO / 2.0 ECTS)

Bachelorstudium Informatik (SKZ: 521, Version: 03W.1)
- Fach: Spezifikation und Verifikation (Pflichtfach)
  - Spezifikation und Verifikation ( 2.0h VO / 2.0 ECTS)
    - 622.050 Spezifikation und Verifikation (2.0h VO / 2.0 ECTS)

Masterstudium Informatik (SKZ: 921, Version: 09W.1)
- Fach: Spezifikation und Verifikation (Pflichtfach)
  - Spezifikation und Verifikation ( 2.0h VO / 2.0 ECTS)
    - 622.050 Spezifikation und Verifikation (2.0h VO / 2.0 ECTS)

Masterstudium Informatik (SKZ: 921, Version: 03W.1)
- Fach: Spezifikation und Verifikation (Pflichtfach)
  - Spezifikation und Verifikation ( 2.0h VO / 2.0 ECTS)
    - 622.050 Spezifikation und Verifikation (2.0h VO / 2.0 ECTS)

Diplomstudium Informatik (SKZ: 880, Version: 02W)
- 2.Abschnitt
  - Fach: Angewandte Informatik inkl. Vertiefungsfach (Pflichtfach)
    - Spezifikation und Verifikation ( 2.0h VO / 2.0 ECTS)
      - 622.050 Spezifikation und Verifikation (2.0h VO / 2.0 ECTS)

Diplomstudium Informatik (SKZ: 880, Version: 02W)
- 3.Abschnitt
  - Fach: Angewandte Informatik und Vertiefungsfach (Pflichtfach)
    - Spezifikation und Verifikation ( 2.0h VO / 2.0 ECTS)
      - 622.050 Spezifikation und Verifikation (2.0h VO / 2.0 ECTS)

Gleichwertige Lehrveranstaltungen im Sinne der Prüfungsantrittszählung

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)