Feature-orientierte Verifikation von Softwareproduktlinien
Final Report Abstract
Eine Softwareproduktlinie ist eine Menge von Produktvarianten mit wohldefinierten Gemeinsamkeiten und Unterschieden. Die Softwareproduktlinienentwicklung zielt darauf ab, diese Menge von Produktvarianten durch systematische Wiederverwendung zu erstellen. Aufgrund der hohen Konfigurierbarkeit der Produktvarianten ist es wichtig, ihre Qualität sicherzustellen. Wegen ihrer hohen Anzahl ist es jedoch im allgemeinen nicht möglich, jede Variante einzeln zu überprüfen. Daher werden Verifikationstechniken für Softwareproduktlinien benötigt, die den Verifikationsaufwand reduzieren und Verifikationsartefakte so wiederverwenden, dass die Produktlinie effizient geprüft werden kann. Im Forschungsvorhaben "Feature-orientierte Verifikation von Softwareproduktlinien" wurden inkrementelle und kompositionale Verifikationstechniken entwickelt, um die Qualität von Softwareproduktlinien effizient sicherzustellen. Eine Grundlage dafür ist die Beschreibung aller Produktvarianten einer Produktlinie durch das neuartige Konzept der Delta-Modellierung. Eine Menge von Produktvarianten wird hierbei durch ein ausgezeichnetes Kernprodukt und eine Menge von Deltas repräsentiert, die das Kernprodukt verändern. Um eine bestimmte Produktvariante zu erhalten, muss eine ausgewählte Menge von Deltas auf das Kernprodukt angewendet werden. So kann aus dem Kernprodukt und seiner Spezifikation eine Produktvariante und ihre zugehörige Spezifikation erzeugt werden. Anders als bisher existierende Variabilitätsmodellierungskonzepte verbindet die Delta-Modellierung Ausdrucksstärke in der Variabilitätsbeschreibung mit einer modularen Repräsentation. Damit legt die Delta-Modellierung den Grundstein für eine inkrementelle Verifikation von Produktvarianten. Ausgehend von einem verifizierten Kernprodukt kann nur durch Analyse der Deltas, die zur Erzeugung einer weiteren Produktvariante venwendet werden, erschlossen werden, welche Verifikationsaufgaben für diese Produktvariante zu zeigen sind und welche Eigenschaften des Kernprodukts nach der Delta-Anwendung unverändert gelten. Für jedes Delta, das für die Variantenerzeugung benutzt wird, kann diese Analyse separat durchgeführt und für das Endresultat komponiert werden. Als alternatives Variabilitätsmodellierungskonzept für Softwareproduktlinien wurde zudem die hierarchische Variabilitätsmodellierung entwickelt. Hierbei wird eine Menge von Produktvarianten durch ihre gemeinsamen Anteile und eine (möglicherweise leere) Menge von Variationspunkten beschrieben. Für jeden Variationspunkt gibt es eine Menge von Varianten, die beschreiben, wie ein Variationspunkt realisiert werden kann. Die Varianten werden durch die gleiche Struktur repräsentiert, so dass ein hierarchisches Modell entsteht. Diese hierarchische Variabilitätsrepräsentation eignet sich äußerst gut für die kompositionale Verifikation. Jede Hierarchieebene kann einzeln bezüglich gewisser Annahmen analysiert werden, was zu einer Verifikationstechnik mit linearer Komplexität in der Modellgröße führt.
Publications
- Compositional Type-Checking for Delta-oriented Programming. Intl. Conference on Aspect-oriented Software Development (AOSD'11), Porto de Galinihas, Brasil, March 21-25, 2011
I. Schaefer, L. Bettini, F. Damiani
- Formal Methods in Software Product Line Engineering, IEEE Computer, February 2011
I. Schaefer, R. Hähnle
- Verification of Software Product Lines with Deltaoriented Slicing. International Conference on Formel Verification of Object-oriented Software (FoVeOOS 2010), Springer, LNCS 6528, 2011
D. Bruns, V. Klebanov, I. Schaefer
