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

Software-Verifikation - Detailseite

  • Funktionen:
Grunddaten
Veranstaltungsart Vorlesung Veranstaltungsnummer 3313034
Semester SoSe 2020 SWS 4
Rhythmus Moodle-Link  
Veranstaltungsstatus Freigegeben für Vorlesungsverzeichnis  Freigegeben  Sprache deutsch
Belegungsfristen Es findet keine Online-Belegung über AGNES statt!
Veranstaltungsformat digital

Termine

Gruppe 1
Tag Zeit Rhythmus Dauer Raum Raum-
plan
Lehrperson Status Bemerkung fällt aus am Max. Teilnehmer
Mi. 13:00 bis 15:00 wöch Johann von Neumann-Haus - 3.113 Rudower Chaussee 25 (RUD25) - (Unterrichtsraum) Schlingloff findet statt     1000
Do. 13:00 bis 15:00 wöch Johann von Neumann-Haus - 3.113 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
Bachelor of Science  Info, Mathe und Physik Monobachelor ( Vertiefung: kein LA; POVersion: 2019 )     -  
Bachelor of Arts  Informatik Kernfach ( POVersion: 2004 )   -  
Bachelor of Arts  Informatik Kernfach ( POVersion: 2010 )   -  
Bachelor of Science  Informatik Kernfach ( Vertiefung: mit LA-Option; POVersion: 2015 )   -  
Bachelor of Science  Informatik Kernfach ( Vertiefung: kein LA; POVersion: 2015 )   -  
Bachelor of Science  Informatik Monobachelor ( Vertiefung: kein LA; POVersion: 2015 )   -  
Bachelor of Arts  Informatik Zweitfach ( POVersion: 2010 )   -  
Bachelor of Science  Informatik Zweitfach ( Vertiefung: kein LA; POVersion: 2015 )   -  
Bachelor of Arts  Informatik Zweitfach ( Vertiefung: mit LA-Option; POVersion: 2015 )   -  
Bachelor of Science  Informatik Zweitfach ( Vertiefung: mit LA-Option; POVersion: 2015 )   -  
Bachelor of Arts  Informatik Zweitfach ( Vertiefung: kein LA; POVersion: 2015 )   -  
Bachelor of Arts  Informationsman. & -tech. Monobachelor ( Vertiefung: kein LA; POVersion: 2015 )   -  
Bachelor of Arts  Informationsman. & -tech. Monobachelor ( Vertiefung: kein LA; POVersion: 2017 )   -  
Zuordnung zu Einrichtungen
Einrichtung
Mathematisch-Naturwissenschaftliche Fakultät, Institut für Informatik
Inhalt
Kommentar

Je mehr Software in sicherheitskritischen Systemen eingesetzt wird, umso wichtiger wird es, ihre Korrektheit objektiv nachzuweisen. Beispiele sind Signalisierungsanlagen in der Bahntechnik, Steuercomputer in Flugzeugen oder Regelungen medizinischer Geräte. In den letzten Jahren sind formale Verifikations- und Analysemethoden für solche Software so weit entwickelt worden, dass sie auch für industriell relevante Probleme einsetzbar geworden sind. Zu den Eigenschaften, die formal nachweisbar sind, gehören z.B. die Abwesenheit von arithmetischen Überläufen bzw. Nulldivisionen, Speicherfehlern, oder „toten“ Codes. Der Einsatz dieser Methoden wird von den einschlägigen Normen für hochgradig sicherheitsrelevante Software dringend empfohlen. Aber auch bei der Entwicklung von Treibern und Standardsoftware für weitverbreitete Betriebssysteme werden statische und dynamische Analysewerkzeuge eingesetzt.
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: 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.


Die Vorlesung gibt einen Überblick über die wichtigsten formalen Methoden zur Software-Verifikation. In den Übungen erlernen die Teilnehmer anhand verschiedener Werkzeuge, wie die entsprechenden Methoden in der Praxis eingesetzt werden können.

Strukturbaum

Die Veranstaltung wurde 1 mal im Vorlesungsverzeichnis SoSe 2020 gefunden:

Humboldt-Universität zu Berlin | Unter den Linden 6 | D-10099 Berlin