FAKULTÄT FÜR

INFORMATIK

Verification of Software Product Lines Using Contracts

Eine Herausforderung in der Softwaretechnik ist die Korrektheit von Software sicherzustellen. Die Verifikation von Software ist zunehmend von Bedeutung, da Software immer mehr in eingebetteten Systemen eingesetzt wird. Beispielsweise können Fehlfunktionen in Fahrzeugen oder Produktionsanalagen katastrophale Auswirkungen haben. Seit etwa 60 Jahren werden Methoden zur Softwareverifikation entwickelt, jedoch betrachten diese meist nur ein Softwaresystem. Doch oft gibt es von einer Software mehrere Varianten, die auf bestimmte Anforderungen maßgeschneidert sind (z.B. verschiedene Modelle eines Fahrzeugs). Die Varianten einer Software werden auch als Softwareproduktlinie bezeichnet.

Ziel der Doktorarbeit ist die Entwicklung von Methoden zur effizienten Verifikation von Softwareproduktlinien. Die wichtigste Grundlage für die Verifikation von Software ist die Spezifikation des gewünschten Verhaltens. In der geplanten Doktorarbeit werden hierzu Methodenkontrakte verwendet, welche die vom Methodenaufrufer zu erfüllenden Vorbedingungen und die von der Methode zu erfüllenden Nachbedingungen festlegen. In mehreren Fallstudien konnte bereits gezeigt werden, dass Kontrakte zur effizienten Spezifikation und Verifikation von Softwareproduktlinien geeignet sind.