Evolutionary Verification of Consistency Properties in Software Product Lines
Evolutionäre Verifikation von Konsistenzeigenschaften in Software-Produktlinien
- A Software Product Line (SPL) realizes a set of related products, which share a common infrastructure, but vary in individual capabilities. This variability enables extensive reuse of customizable artifacts to create specific product variants per customer. This reuse in turn provides significant benefits, like higher quality of these shared artifacts and faster time-to-market of product variants. At the same time, variability introduces its own complexity as it is typically scattered across a plethora of artifacts, like code and build files. Hence, verification approaches for SPLs aim at detecting variability-related defects and inconsistencies, which lead to invalid products. In general, verification takes a significant amount of time to provide complete results for an entire, complex SPL. The main reason for this delay resides in the same variability enabling the beneficial reuse in a SPL. SPL verification approaches therefore have to consider multiple variants of thousands of artifacts. If the SPL evolves, previous analysis results potentially become invalid. Hence, ensuring correctness and consistency continuously requires the same entire verification effort again for each increment. In particular, this situation during SPL evolution is not reasonable in practice due to recurring (potentially longer) delays for even minor changes. This dissertation introduces an incremental approach to evolutionary verification of SPLs to avoid unnecessary analysis effort based on an upfront change relevance analysis. It leverages the results of this upfront analysis to update its previous verification results partially by re-verifying changed artifacts only. In particular, it combines raw change information (unmodified commit data) with the unmodified core analysis of a verification. The foundation for this combination are the results of two studies of the evolution of different SPLs. They reveal that changes to the variability of a SPL occur infrequently and only affect small parts of the analyzed artifacts. These new insights lead to the introduced incremental approach, which reuses the algorithm of these studies for its upfront change relevance analysis. A performance analysis of specific variants of this incremental approach with their non-incremental original demonstrates an acceleration of the median verification time by up to factor 319. A discussion of the impact of these variant on the overall performance provides further insights into optimization that are worthwhile. A description of the practical applicability of the presented approach offers several opportunities to support developers during SPL evolution.
- Eine Software-Produktlinie (SPL) besteht aus einer Menge verwandter Produkte, die eine gemeinsame Infrastruktur nutzen, aber in ihren individuellen Fähigkeiten variieren. Diese Variabilität ermöglicht eine umfassende Wiederverwendung der anpassbaren Artefakte zur Erstellung spezifischer Produktvarianten für jeden Kunden. Diese Wiederverwendung bietet wiederum signifikante Vorteile. Zum Beispiel erhöht sie die Qualität der wiederverwendeten Artefakte und beschleunigt die Markteinführung von Produktvarianten. Gleichzeitig bringt die Variabilität ihre eigene Komplexität mit sich, da sie typischerweise über eine Vielzahl von Artefakten, wie Code und Build-Dateien, verstreut ist. Daher zielen Verifikationsansätze für SPLn darauf ab, variabilitätsbedingte Fehler und Inkonsistenzen zu erkennen, die zu ungültigen Produkten führen. Im Allgemeinen benötigt die Verifikation sehr viel Zeit, um vollständige Ergebnisse für eine gesamte, komplexe SPL zu liefern. Der Hauptgrund für diese Verzögerung liegt in der gleichen Variabilität, die die vorteilhafte Wiederverwendung in einer SPL ermöglicht. Verifikationsansätze für SPLn müssen daher mehrere Varianten von Tausenden von Artefakten berücksichtigen. Wenn sich die SPL dann weiterentwickelt, werden frühere Analyseergebnisse möglicherweise ungültig. Die Sicherstellung von Korrektheit und Konsistenz erfordert daher für jedes Inkrement erneut den gleichen gesamten Verifikationsaufwand. Insbesondere während der Evolution von SPLn ist diese Situation in der Praxis nicht sinnvoll, da selbst bei kleinen Änderungen immer wieder (potenziell längere) Verzögerungen auftreten. Diese Dissertation führt einen inkrementellen Ansatz zur evolutionären Verifikation von SPLn ein, um unnötigen Analyseaufwand auf der Basis einer vorgelagerten Untersuchung der Relevanz von Änderungen zu vermeiden. Der Ansatz nutzt die Ergebnisse dieser vorgelagerten Untersuchung, um die bisherigen Verifikationsergebnisse teilweise zu aktualisieren, indem nur geänderte Artefakte erneut verifiziert werden. Insbesondere kombiniert der Ansatz unbearbeitete Änderungsinformationen (unveränderte Commit-Daten) mit der unveränderten Kernanalyse einer Verifikation. Grundlage für diese Kombination sind die Ergebnisse von zwei Studien über die Evolution verschiedener SPLn. Diese Studien zeigen, dass Änderungen an der Variabilität einer SPL nur selten auftreten und ausschließlich kleine Teile der analysierten Artefakte betreffen. Diese neuen Erkenntnisse führen zu dem vorgestellten inkrementellen Ansatz, der den Algorithmus dieser Studien für die vorgelagerte Untersuchung der Relevanz von Änderungen wiederverwendet. Eine Performanz-Analyse spezifischer Varianten dieses inkrementellen Ansatzes mit ihrem nicht inkrementellen Original zeigt eine Beschleunigung der mittleren Verifikationszeit (Median) um bis zu Faktor 319. Eine Diskussion der Auswirkungen dieser Varianten auf die Performanz im Allgemeinen liefert weitere Erkenntnisse hinsichtlich lohnenswerter Optimierungen. Eine Beschreibung der praktischen Anwendbarkeit des vorgestellten Ansatzes stellt mehrere Möglichkeiten vor, wie Entwickler während der Evolution von SPLn unterstützt werden können.
Author: | Christian Kröher |
---|---|
URN: | https://nbn-resolving.org/urn:nbn:de:gbv:hil2-opus4-17686 |
DOI: | https://doi.org/10.25528/181 |
Referee: | Klaus Schmid, Rick Rabiser |
Advisor: | Klaus Schmid |
Document Type: | Doctoral Thesis |
Language: | English |
Year of Completion: | 2023 |
Publishing Institution: | Stiftung Universität Hildesheim |
Granting Institution: | Universität Hildesheim, Fachbereich IV |
Date of final exam: | 2023/10/25 |
Release Date: | 2023/11/15 |
Page Number: | 167 |
PPN: | Link zum Katalog |
Institutes: | Fachbereich IV |
Licence (German): | ![]() |