AGNES -
Lehre und Prüfung online
Studierende in Vorlesung
Anmelden

Verifikation von Software - Detailseite

  • Funktionen:
Grunddaten
Veranstaltungsart Vorlesung Veranstaltungsnummer 3313049
Semester WiSe 2023/24 SWS 4
Rhythmus Moodle-Link  
Veranstaltungsstatus Freigegeben für Vorlesungsverzeichnis  Freigegeben  Sprache deutsch
Belegungsfrist Es findet keine Online-Belegung über AGNES statt!
Veranstaltungsformat Keine Angabe

Termine

Gruppe 1
Tag Zeit Rhythmus Dauer Raum Raum-
plan
Lehrperson Status Bemerkung fällt aus am Max. Teilnehmer/-innen
Di. 09:00 bis 11:00 wöch Johann von Neumann-Haus - 3.113 Rudower Chaussee 25 (RUD25) - (Unterrichtsraum) Schlingloff findet statt     1000
Do. 09:00 bis 11:00 wöch Johann von Neumann-Haus - 4.112 Rudower Chaussee 25 (RUD25) - (Unterrichtsraum) Schlingloff findet statt     1000
Gruppe 1:
 


Zugeordnete Person
Zugeordnete Person Zuständigkeit
Prof. Dr. Schlingloff, Holger
Studiengänge
Abschluss Studiengang LP Semester
Master of Education (BS)  Informatik 2. Fach ( Vertiefung: mit LA-Option; POVersion: 2015 )   -  
Master of Education (GYM)  Informatik 2. Fach ( Vertiefung: mit LA-Option; POVersion: 2015 )   -  
Master of Education (ISG)  Informatik 1. Fach ( Vertiefung: mit LA-Option; POVersion: 2018 )   -  
Master of Education (ISG)  Informatik 2. Fach ( Vertiefung: mit LA-Option; POVersion: 2018 )   -  
Master of Science  Informatik Hauptfach ( Vertiefung: kein LA; POVersion: 2015 )   -  
Master of Science  Wirtschaftsinformatik Hauptfach ( Vertiefung: kein LA; POVersion: 2016 )   -  
Zuordnung zu Einrichtungen
Einrichtung
Mathematisch-Naturwissenschaftliche Fakultät, Institut für Informatik
Inhalt
Kommentar

Um sicherheitskritische Systeme in der Praxis einsetzen zu können, muss die Korrektheit der Software objektiv nachgewiesen werden. Zur Zulassung von Systemen wie etwa Signalisierungsanlagen in der Bahntechnik, Steuercomputer in Flugzeugen oder Regelungen medizinischer Geräte empfehlen die einschlägigen Normen (EN 61508, EN 50128 oder DO-178C) den Einsatz formaler Methoden. In den letzten Jahren sind formale Verifikations- und Analysemethoden so weit entwickelt worden, dass sie auch für Probleme von industriell relevanter Größe einsetzbar geworden sind. Bei der Modellprüfung (Model Checking) wird ein Modell des Systems bezüglich einer temporallogischen Eigenschaft überprüft, und bei der dynamischen Analyse werden Laufzeiteigenschaften bezüglich spezifizierter Anforderungen untersucht. Zu den Eigenschaften, die formal nachweisbar sind, gehören z.B. die Abwesenheit von arithmetischen Überläufen bzw. Nulldivisionen oder die Erreichbarkeit von Fehlerzuständen und Lokalisierung „toten“ Codes. Ein neues Gebiet ist der Sicherheitsnachweis für lernende und adaptive Systeme.

Das Modul behandelt Methoden zur deduktiven Verifikation, bei der die Beweise interaktiv vom Benutzer mit einem Beweissystem geführt werden, sowie automatische Verifikationsverfahren, die in der industriellen Praxis eingesetzt werden.

Die Vorlesung gibt einen Überblick über die wichtigsten formalen Methoden zur Software-Verifikation.

In den Übungen erlernen die Teilnehmer, wie die entsprechenden Methoden in der Praxis eingesetzt werden können. Es wird das praktische Arbeiten und der Umgang mit verbreiteten Werkzeugen der Verifikation von Software geübt.

In Abgrenzung zum Bachelor-Modul W09-01 (Software-Verifikation) geht dieses Master-Modul auch auf neuere Techniken wie Abstraktionsverfeinerung anhand von Gegenbeispielen, erweiterte temporale Logiken, Erfüllbarkeit modulo Theorien und die Verifikation neuronaler Netze ein.
Die Teilnahme am Bachelor-Modul ist explizit nicht Voraussetzung für die Teilnahme an diesem Master-Modul; eine Teilnahme an beiden Modulen ist nicht möglich.

Strukturbaum

Keine Einordnung ins Vorlesungsverzeichnis vorhanden. Veranstaltung ist aus dem Semester WiSe 2023/24. Aktuelles Semester: SoSe 2024.
Humboldt-Universität zu Berlin | Unter den Linden 6 | D-10099 Berlin