FB3 AG BKB CXL

Inhalt:

• Inhaltliches
• Organisatorisches
• Links

Formale Methoden der Softwaretechnik II

Willkommen auf der Heimatseite der Lehrveranstaltung "Formale Methoden der Softwaretechnik II" im Sommersemester 2006!

Inhaltliches

Diese Veranstaltung ist eine Vertiefung der Verstanstaltung Formale Methoden der Softwaretechnik I vom letzten Semester. Inhalt der Veranstaltung sind damit weiterhin die formale Methoden, d.h. auf der Mathematik (speziell formaler Logik) basierende Methoden zur Sicherstellung der Korrektheit von Software.

Im Gegensatz zum ersten Teil, der einen breiten Überblick über die verwendeten Methoden sowie einen Einblick in die theoretischen Grundlagen geben wollte, werden wir in diesem Teil zwei Aspekte in der Tiefe betrachten, nämlich die Verifikation und die korrekte Programmentwicklung.

Themen

In der Veranstaltung werden folgende Themen behandelt:

• Programmverifikation:
  • Floyd-Hoare-Logik (zur Wiederholung),
  • Prädikatentransformer,
  • Generation von Verifikationsbedingungen,
  • Modellierung von imperativen Programmen,
  • Verifikationswerkzeuge
• Entwicklung korrekter Programme:
  • Entwicklung von korrekten Programmen durch Transformation,
  • Algorithmendesign,
  • Transformationswerkzeuge

Organisatorisches

VAK: 03-05-H-604.04.
Kategorie: V, ECTS: 6.
Modulbereich: Theorie

Termine:

• Vorlesung: Di 10-- 12, MZH 8090. Achtung, geänderter Termin!
• Übungen: Do 9 s.t. -- 10, MZH 6240. Am 27.04.06 findet noch keine Übung statt!
• Veranstaltungsbeginn (erste, außerplanmäßige Vorlesung): Do 20.04.2006 09:00

Achtung: Wegen starker inhaltlicher Überschneidungen kann dieses Modul nicht gleichzeitig mit dem Modul "Techniken zur Entwicklung korrekter Software II" angerechnet werden.

Voraussetzungen

Formale Methoden der Softwaretechnik I ist keine formale Voraussetzung zum Besuch der Veranstaltung, aber der zweite Teil baut natürlich auf dem Inhalt des ersten Teils auf, insbesondere den Grundlagen (formale Logik und Semantik). Diese Kentnisse können auch in anderen Veranstaltungen, z.B. Logik für Informatiker, erworben worden sein.

Vorlesungsfolien

• Alle Folien im Überblick: [PDF] (Fassung vom 18.07.06; wird ständig aktualisiert).
• Handouts pro Vorlesung (PostScript schwarz-weiß, 8 Folien auf einer Seite, zum Ausdrucken):
  
  • [1] vom 25.04.2006.
  • [2] vom 02.05.2006.
  • [3] vom 09.05.2006.
  • [4] vom 16.05.2006.
  • [5] vom 23.05.2006.
  • [6] vom 30.05.2006.
  • [7] vom 06.06.2006.
  • [8] vom 13.06.2006.
  • [9] vom 20.06.2006.
  • [10] vom 27.06.2006.
  • [11] vom 04.07.2006.
  • [12] vom 11.07.2006.
  • [13] vom 18.07.2006.
• Weiteres Material:
  
  • Der Beispielbeweis im Hoare-Kalkül aus der ersten Vorlesung.

Links

• Formale Methoden der Softwaretechnik I

Last modified: Tue May 30 11:56:13 CEST 2006