Dokument-Version: 4.001.03.2021pre

Fakultät Ingenieurwissenschaften

Masterstudiengang (EIM) - Elektrotechnik und Informationstechnik

Formale Verifikation

Kennzahl 8430

Dozententeam

Pflichtmodul 8430

verantwortlich: Prof. Dr. rer. nat. habil. Alfons Geser
Regelsemester Sommersemester 2. Semester (jährlich)
Leistungspunkte *) 5   (Wichtung der LP =5)
Unterrichtssprache Deutsch
Arbeitsaufwand Vorlesung-Präsenz: 28 h; Vorlesung-Vorarbeit: 47 h; Praktikum-Präsenz: 28 h; Praktikum-Vorarbeit: 47 h;
Voraussetzungen für die Teilnahme Kenntnisse/Fähigkeiten: Grundlagen der Informatik (Bachelor)
Lernziel/ Kompetenz Ziel: Vermittlung von vertieftem und erweitertem Fachwissen in der fachspezifischen Informatik und der Mechatronik, insbesondere Korrektheit von HW/SW-Systemen mathematisch beweisen. Einblick in di Aussagenlogik, Prädikatenlogik, Temporale Logik und Lambda-Kalkül

Fach- und methodische Kompetenz: Fähigkeit eine Formale Spezifikation zu entwerfen; Fähigkeit eine Behauptung in PVS zu formalisieren; Fähigkeit einen Beweis zu entwerfen und ihn PVS auszuführen. Einsicht, daß Axiome Widersprüche verursachen können und daß Verschärfung einer Behauptung zielführend sein kann.

Einbindung in die Berufsvorbereitung: Formale Verifikation ist eine leistungsfähige, gut erforschte Methode zur Qualitätssicherung.
Inhalt 1. Grundbegriffe

2. Logische Grundlagen;

3. PVS-Spezifikationssprache;

4. Beweistaktiken;

5. Lambda-Kalkül;

6. Induktion und Rekursion;

7. PVS Prelude;

8. Modelchecking

Prüfungsvorleistungen PVB (Beleg)
Studien- und Prüfungsleistungen
Lehreinheiten SWS Prüfungsleistung Wichtung
V P
Formale Verifikation 2 2 PM 30 min 5
Medienformen Tafel, Overheadprojektor
Literatur
Verwendbarkeit Das Modul ist im Masterstudiengang Elektrotechnik und Informationstechnik verwendbar.