Universität Bremen
FB3 DFKI SKS AG BKB

Techniken zur Entwicklung Korrekter Software 1

Willkommen auf der Heimatseite der Lehrveranstaltung "Techniken zur Entwicklung Korrekter Software 1" im Wintersemester 2007/2008!

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 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). Formale Methoden sind allerdings immer eng mit Techniken des formalen Beweisens verbunden, denn nur durch rechnergestützte Beweise läßt sich die für diesen Bereich nötige durchgängige Korrektheit sicherstellen.

Diese Veranstaltung soll in die nötigen theoretischen Grundlagen einführen, einen Überblick über das Gebiet geben, so dass Teilnehmer formale Methoden in zukünftigen Projekten selber einsetzen können. Schwerpunkte der Veranstaltung sind Anforderungsspezifikationen, Entwurfsspezifikationen und formale Entwicklung, die Spezifikationssprache CASL und Techniken des rechnergestützten, formalen Beweisens.

Themen

In der Vorlesung werden folgende Themen behandelt:

Im Übungsbetrieb werden wir die Spezifikationssprache CASL, den Theorembeweiser Isabelle und das Hets-Werkzeug benutzen.

Organisatorisches

Die Veranstalter sind Lutz Schröder und Christoph Lüth.

VAK: 03-05-H-706.05.
K 4 SWS (6 ECTS) Praxis (A), Handelsklasse: I

Termine:

Wegen starker inhaltlicher Überschneidungen kann dieses Modul nicht gleichzeitig mit dem Modul "Formale Methoden der Softwaretechnik I" angerechnet werden.

Vorlesungsfolien