Universität Bremen
FB3 AG BKB CXL

Formale Methoden der Softwaretechnik

Willkommen auf der Heimatseite der Lehrveranstaltung "Formale Methoden der Softwaretechnik " im Wintersemester 2009/2010!

Inhaltliches

Inhalt der Veranstaltung sind sogenannte Formale Methoden. Hierunter versteht man ganz allgemein Methoden, die Korrektheit von Software mit mathemathischen Mitteln (meist formaler Logik) sicherstellt. Als formale Methoden im engeren Sinne (und im Sinne dieser Veranstaltung) zählen alle Methoden, die auch eine wohldefinierte mathematische Fundierung haben, also zählt zum Beispiel die UML nicht dazu.

Formale Methoden werden je wichtiger, je mehr sicherheitskritische Funktionen in Software (anstatt in Hardware) implementiert werden. In immer mehr Situationen sind Softwarefehler inakzeptabel, und wir müssen die Sicherheit der Software mit anderen Mitteln sicherstellen als code review ("scharf hingucken") oder testen (durch Tests alleine läßt sich nie die Fehlerfreiheit sicherstellen).

Generell können formale Methoden in drei Bereichen helfen: bei der Modellierung und Spezifikation, bei Entwurf und Implementation, und bei der Verifikation.

Diese Veranstaltung soll in die nötigen theoretischen Grundlagen einführen, einen Überblick über das Gebiet geben, und die Anwendung an kleineren Beispielen üben. Im übungsbetrieb werden wir auf den interaktiven Theorembeweiser Isabelle zurückgreifen.

Organisatorisches

Die VAK der Veranstaltung ist 03-05-H-604.03.

Termine

Achtung: Die Veranstaltung am 04.11. entfällt!

Scheinkriterien

Vorlesungsfolien

Die Vorlesungsfolien sind jeweils verfügbar als ganzseitiges PDF zum Betrachten, oder als 8:1 Handzettel ohne Effekte zum Drucken:

Übungsblätter

Hier finden sich die Übungsblätter zur Veranstaltung.

Literatur und Links

Links zu Isabelle