Spezifikation und Verifikation von Produktlinien mit Feature-orientierten Verträgen

Abstract

Variabilität ist allgegenwärtig in der heutigen Softwareentwicklung. Während Techniken zur effizienten Implementierung von Software-Produktlinien seit Jahrzehnten eingesetzt werden, waren Verifikationstechniken ein Forschungsschwerpunkt in den letzten Jahren. Wir geben eine Übersicht darüber, wie existierende Verifikationstechniken auf Produktlinien angewandt worden. Mithilfe unserer Erkenntnisse beheben wir zwei Defizite früherer Forschungsarbeiten. Ei- nerseits untersuchen wir systematisch wie Verträge zur Produktlinienspezifikation genutzt werden können. Unsere theoretische Diskussion und praktische Evaluierung führt uns zum Konzept der Feature-orientierten Verträge. Insbesondere haben wir beobachtet, dass viele aber nicht alle Featureorientierten Verträge dem liskovschen Substitutionsprinzip folgen. Anderseits nutzen wir Featureorientierte Verträge zum Vergleich verschiedener Verifikationstechniken und -strategien für dieselbe Produktlinienimplementierung und -spezifikation. Bei der Kombination von Theorembeweisern und Modellprüfern konnten wir Synergien für die Produktlinienverifikation messen.