Lecture: Formale Methoden im Software Engineering - Details

Lecture: Formale Methoden im Software Engineering - Details

You are not logged into Stud.IP.

General information

Course name Lecture: Formale Methoden im Software Engineering
Course number INF-0130, INF-0229
Semester SS 2024
Current number of participants 23
expected number of participants 30
Home institute Softwaretechnik
Courses type Lecture in category Teaching
First date Wednesday, 17.04.2024 12:15 - 13:45, Room: (1054 N)
Type/Form Vorlesung mit integriertem Praktikum
Pre-requisites Interesse an Logik und formalen Methoden, Bachelorveranstaltung Logik für Informatiker ist hilfreich
Veranstaltung findet in Präsenz statt / hat Präsenz-Bestandteile Yes
Hauptunterrichtssprache deutsch
Literaturhinweise Es besteht eigentlich keine Notwendigkeit, zusätzliche Literatur heranzuziehen. Wer sich dennoch etwas schlauer machen will, kann folgende Bücher lesen:
- V. Sperschneider and G. Antoniou, Logic: A Foundation for Computer Science, Addison Wesley, 1991
- J. Loeckx and H.D. Ehrich and M. Wolf, Specification of Abstract Data Types, Wiley-Teubner, 1996
ECTS points 8

Rooms and times

(1054 N)
Wednesday: 12:15 - 13:45, weekly (12x)
(3017 N)
Friday: 10:00 - 13:00, weekly (12x)
Friday: 14:00 - 17:00, weekly (12x)
Friday, 03.05.2024 10:00 - 11:30
Friday, 03.05.2024 14:00 - 15:30

Module assignments

Comment/Description

Die Verwendung formaler Methoden bei der Entwicklung korrekter Software steht an der Schwelle der kommerziellen Nutzung. Das KIV-System ist ein Werkzeug, das die formale Spezifikation, Verifikation und Synthese von Programmen ermöglicht. Es wird seit mehreren Jahren entwickelt und inzwischen in industriellen Studien erprobt. Übergeordnetes Ziel ist die Produktion beweisbar korrekter Software.

Die Lehrveranstaltung vermittelt den ''state of the Art'' des Einsatzes formaler Methoden bei der Softwareentwicklung. Es werden Spezifikationstechniken zur Beschreibung und Methoden zum Nachweis der Korrektheit von Softwaresystemen behandelt. Die Lehrveranstaltung beginnt mit der (algebraischen) Spezifikation von Datentypen und stellt dann Kalküle und Vorgehensweisen für die Verifikation sequentieller und paralleler Programme vor. Weiterhin wird Refinement als systematisches Entwicklungsvorgehen von einer abstrakten Spezifikation zu einer korrekten Implementierung vorgestellt.

Die Rechner im Raum 3017N stehen auch außerhalb der Praktikumszeiten zur Verfügung. Notfalls bei uns nach einem Schlüssel fragen, falls der Raum abgesperrt ist.