622.051 (15W) Spezifikation und Verifikation

Wintersemester 2015/16

Anmeldefrist abgelaufen.

Erster Termin der LV
06.10.2015 13:00 - 15:00 , HS 3 On Campus
... keine weiteren Termine bekannt

Überblick

Lehrende/r
LV-Titel englisch
Specification and Verification
LV-Art
Übung (prüfungsimmanente LV )
Semesterstunde/n
2.0
ECTS-Anrechnungspunkte
4.0
Anmeldungen
16 (25 max.)
Organisationseinheit
Unterrichtssprache
Deutsch
LV-Beginn
06.10.2015
eLearning
zum Moodle-Kurs

Zeit und Ort

Liste der Termine wird geladen...

LV-Beschreibung

Lehrmethodik inkl. Einsatz von eLearning-Tools

Gemeinsames Erarbeiten anhand von kleinen Aufgaben, teilweise in den Computerlabors.

Inhalt/e

Diese Lehveranstaltung ist eng an die Vorlesung Spezifikation und Verifikation gekoppelt und ergänzt deren Lehrinhalte durch praktische Anwendungsbeispiele.

Themen

  • Spezifikationssprache Z
  • Mengen, Multimengen, Relationen
  • Beweise
  • Code-Generierung

Lehrziel

Verstehen und Entwerfen von Z Spezifikationen (Zustandsraum, Initialzustand, Operations-Schemata). Verstehen und Durchführen von formalen Beweisen.

Erwartete Vorkenntnisse

Paralleler Besuch der Vorlesung Spezifikation und Verifikation.

Sonstige Studienbehelfe

Die in der LV verwendeten Z Spezifikationen werden mittels Latex und Eclipse erzeugt und sind auf jedem Rechner editierbar.

Literatur

Antoni Diller. Z An Introduction to Formal Methods. 2nd Ed. John Wiley & Sons. 1994. Jonathan Jacky. The Way of Z. Cambridge University Press. 1997.

Lehrmethodik inkl. Einsatz von eLearning-Tools

Practical examples presented by student groups.

Inhalt/e

This practical class is tightly coupled to the lecture of specification and verification (Prof. Mittermeir).

Themen

  • Specification Language Z
  • Sets, Bags, Relations
  • Code Generation
  • Proofs

Lehrziel

Comprehension and generation of Z specifications (state-schema, initial schema, operation schema) and formal proofs.

Erwartete Vorkenntnisse

Lecture specification and verification.

Sonstige Studienbehelfe

All specifications are generated using Latex and Eclipse, which is a free software and can be run without problems on nearly any system.

Literatur

Antoni Diller. Z An Introduction to Formal Methods. 2nd Ed. John Wiley & Sons. 1994. Jonathan Jacky. The Way of Z. Cambridge University Press. 1997.

Prüfungsinformationen

Beurteilungskriterien/-maßstäbe

Schriftlich, mehrere Mitarbeitsüberprüfungen ohne Unterlagen

Beurteilungskriterien/-maßstäbe

Several tests during the semester. No materials allowed.

Beurteilungsschema

Note/Grade Benotungsschema

Position im Curriculum

  • Lehramtsstudium Unterrichtsfach Informatik und Informatikmanagement (SKZ: 884, Version: 04W.7)
    • 2.Abschnitt
      • Fach: Angewandte Informatik (LI 2.3) (Pflichtfach)
        • Spezifikation und Verifikation ( 2.0h PR / 4.0 ECTS)
          • 622.051 Spezifikation und Verifikation (2.0h UE / 4.0 ECTS)
  • Bachelorstudium Angewandte Informatik (SKZ: 511, Version: 12W.1)
    • Fach: Softwareentwicklung (Wahlfach)
      • Spezifikation und Verifikation ( 2.0h UE / 4.0 ECTS)
        • 622.051 Spezifikation und Verifikation (2.0h UE / 4.0 ECTS)
  • Bachelorstudium Informatik (SKZ: 521, Version: 09W.3)
    • Fach: Spezifikation und Verifikation (Wahlfach)
      • Spezifikation und Verifikation ( 2.0h PR / 4.0 ECTS)
        • 622.051 Spezifikation und Verifikation (2.0h UE / 4.0 ECTS)
  • Bachelorstudium Informatik (SKZ: 521, Version: 03W.1)
    • Fach: Spezifikation und Verifikation (Pflichtfach)
      • Spezifikation und Verifikation ( 2.0h PR / 4.0 ECTS)
        • 622.051 Spezifikation und Verifikation (2.0h UE / 4.0 ECTS)
  • Masterstudium Angewandte Informatik (SKZ: 911, Version: 13W.1)
    • Fach: Vertiefung Informatik (Pflichtfach)
      • Spezifikation und Verifikation ( 2.0h UE / 4.0 ECTS)
        • 622.051 Spezifikation und Verifikation (2.0h UE / 4.0 ECTS)
  • Masterstudium Informatik (SKZ: 921, Version: 09W.1)
    • Fach: Spezifikation und Verifikation (Pflichtfach)
      • Spezifikation und Verifikation ( 2.0h PR / 4.0 ECTS)
        • 622.051 Spezifikation und Verifikation (2.0h UE / 4.0 ECTS)
  • Masterstudium Informatik (SKZ: 921, Version: 03W.1)
    • Fach: Spezifikation und Verifikation (Pflichtfach)
      • Spezifikation und Verifikation ( 2.0h PR / 4.0 ECTS)
        • 622.051 Spezifikation und Verifikation (2.0h UE / 4.0 ECTS)
  • Diplomstudium Informatik (SKZ: 880, Version: 02W)
    • 2.Abschnitt
      • Fach: Angewandte Informatik inkl. Vertiefungsfach (Pflichtfach)
        • Spezifikation und Verifikation ( 2.0h PR / 4.0 ECTS)
          • 622.051 Spezifikation und Verifikation (2.0h UE / 4.0 ECTS)
  • Diplomstudium Informatik (SKZ: 880, Version: 02W)
    • 3.Abschnitt
      • Fach: Angewandte Informatik und Vertiefungsfach (Pflichtfach)
        • Spezifikation und Verifikation ( 2.0h PR / 4.0 ECTS)
          • 622.051 Spezifikation und Verifikation (2.0h UE / 4.0 ECTS)

Gleichwertige Lehrveranstaltungen im Sinne der Prüfungsantrittszählung

Wintersemester 2020/21
  • 622.051 UE Spezifikation und Verifikation (2.0h / 4.0ECTS)
Wintersemester 2019/20
  • 622.051 UE Spezifikation und Verifikation (2.0h / 4.0ECTS)
Wintersemester 2018/19
  • 622.051 UE Spezifikation und Verifikation (2.0h / 4.0ECTS)
Wintersemester 2017/18
  • 622.051 UE Spezifikation und Verifikation (2.0h / 4.0ECTS)
Wintersemester 2016/17
  • 622.051 UE Spezifikation und Verifikation (2.0h / 4.0ECTS)
Wintersemester 2014/15
  • 622.051 UE Spezifikation und Verifikation (2.0h / 4.0ECTS)
Wintersemester 2013/14
  • 622.051 UE Spezifikation und Verifikation (2.0h / 4.0ECTS)
Wintersemester 2012/13
  • 622.051 PR Spezifikation und Verifikation (2.0h / 4.0ECTS)
Wintersemester 2010/11
  • 622.051 PR Spezifikation und Verifikation (2.0h / 4.0ECTS)
Wintersemester 2009/10
  • 622.051 PR Spezifikation und Verifikation (2.0h / 4.0ECTS)
  • 622.052 PR Spezifikation und Verifikation (2.0h / 4.0ECTS)