TU Darmstadt / ULB / TUbiblio

Automatisierte Analyse integrierter Software-Produktlinien-Spezifikationen

Weckesser, Markus Tobias (2019)
Automatisierte Analyse integrierter Software-Produktlinien-Spezifikationen.
Technische Universität Darmstadt
Dissertation, Erstveröffentlichung

Kurzbeschreibung (Abstract)

Der Trend zur Digitalisierung führt zu neuen Anwendungsszenarien (z.B. Industrie 4.0, Internet der Dinge, intelligente Stromnetze), die laufzeitadaptive Software-Systeme erfordern, die sich durch kontinuierliche Rekonfiguration an verändernde Umgebungsbedingungen anpassen. Integrierte Software-Produktlinien-Spezifikationen ermöglichen die präzise Beschreibung von Konsistenzeigenschaften derartiger Systeme in einer einheitlichen Repräsentation. So bietet die Spezifikationssprache Clafer sowohl Sprachmittel zur Charakterisierung der Laufzeitvariabilität eines Systems als auch für die rekonfigurierbaren Bestandteile der Systemarchitektur sowie komplexer Abhängigkeiten. In Clafer-Spezifikationen werden hierzu Sprachkonstrukte aus UML-Klassendiagrammen und Meta-Modellierungssprachen zusammen mit Feature-orientierten Modellierungstechniken und Constraints in Prädikatenlogik erster Stufe kombiniert. Durch die beträchtliche Ausdrucksstärke neigen derartige integrierte Produktlinien-Spezifikationen in der Praxis dazu, sehr komplex zu werden (z.B. aufgrund versteckter Abhängigkeiten zwischen Konfigurationsoptionen und Komponenten). Sie sind daher äußerst anfällig für Spezifikationsfehler in Form von Inkonsistenzen oder Entwurfsschwächen in Form von Anomalien. Inkonsistenzen und Anomalien müssen jedoch möglichst früh im Entwurfsprozess erkannt und behoben werden, um drastische Folgekosten zur Laufzeit eines Systems zu vermeiden. Aus diesem Grund sind statische Analysetechniken zur automatisierten Analyse integrierter Software-Produktlinien-Spezifikationen unabdingbar.

Existierende Ansätze zur Konsistenzprüfung erfordern, dass der Suchraum für die Instanzsuche vorab entweder manuell oder durch heuristisch identifizierte Schranken eingeschränkt wird. Da, falls keine Instanz gefunden werden kann, nicht bekannt ist, ob dies durch einen zu klein gewählten Suchraum oder eine tatsächliche Inkonsistenz verursacht wurde, sind existierende Analyseverfahren inhärent unvollständig und praktisch nur eingeschränkt nutzbar. Darüber hinaus wurden bisher noch keine Analysen zur Identifikation von Anomalien vorgeschlagen, wie sie beispielsweise in Variabilitätsmodellen auftreten können. Weiterhin erlauben existierende Verfahren zwar die Handhabung von ganzzahligen Attributen, ermöglichen jedoch keine effiziente Analyse von Spezifikationen die zusätzlich reellwertige Attribute aufweisen.

In dieser Arbeit präsentieren wir einen Ansatz zur automatisierten Analyse integrierter Software-Produktlinien-Spezifikationen, die in der Sprache Clafer spezifiziert sind. Hierfür präsentieren wir eine ganzheitliche Spezifikation der strukturellen Konsistenzeigenschaften laufzeitadaptiver Software-Systeme und schlagen neuartige Anomalietypen vor, die in Clafer-Spezifikationen auftreten können. Wir charakterisieren eine Kernsprache, die eine vollständige und korrekte Analyse von Clafer-Spezifikationen ermöglicht. Wir führen zusätzlich eine neuartige semantische Repräsentation als mathematisches Optimierungsproblem ein, die über die Kernsprache hinaus eine effiziente Analyse praxisrelevanter Clafer-Spezifikationen ermöglicht und die Anwendung etablierter Standard-Lösungsverfahren erlaubt. Die Methoden und Techniken dieser Arbeit werden anhand eines durchgängigen Beispiels eines selbst-adaptiven Kommunikationssystems illustriert und prototypisch implementiert. Die experimentelle Evaluation zeigt die Effektivität unseres Analyseverfahrens sowie erhebliche Verbesserungen der Laufzeiteffizienz im Vergleich zu etablierten Verfahren.

Typ des Eintrags: Dissertation
Erschienen: 2019
Autor(en): Weckesser, Markus Tobias
Art des Eintrags: Erstveröffentlichung
Titel: Automatisierte Analyse integrierter Software-Produktlinien-Spezifikationen
Sprache: Deutsch
Referenten: Schürr, Prof. Dr. Andreas ; Becker, Prof. Dr. Christian
Publikationsjahr: 28 Juni 2019
Ort: Darmstadt
Datum der mündlichen Prüfung: 28 Juni 2019
URL / URN: https://tuprints.ulb.tu-darmstadt.de/8875
Kurzbeschreibung (Abstract):

Der Trend zur Digitalisierung führt zu neuen Anwendungsszenarien (z.B. Industrie 4.0, Internet der Dinge, intelligente Stromnetze), die laufzeitadaptive Software-Systeme erfordern, die sich durch kontinuierliche Rekonfiguration an verändernde Umgebungsbedingungen anpassen. Integrierte Software-Produktlinien-Spezifikationen ermöglichen die präzise Beschreibung von Konsistenzeigenschaften derartiger Systeme in einer einheitlichen Repräsentation. So bietet die Spezifikationssprache Clafer sowohl Sprachmittel zur Charakterisierung der Laufzeitvariabilität eines Systems als auch für die rekonfigurierbaren Bestandteile der Systemarchitektur sowie komplexer Abhängigkeiten. In Clafer-Spezifikationen werden hierzu Sprachkonstrukte aus UML-Klassendiagrammen und Meta-Modellierungssprachen zusammen mit Feature-orientierten Modellierungstechniken und Constraints in Prädikatenlogik erster Stufe kombiniert. Durch die beträchtliche Ausdrucksstärke neigen derartige integrierte Produktlinien-Spezifikationen in der Praxis dazu, sehr komplex zu werden (z.B. aufgrund versteckter Abhängigkeiten zwischen Konfigurationsoptionen und Komponenten). Sie sind daher äußerst anfällig für Spezifikationsfehler in Form von Inkonsistenzen oder Entwurfsschwächen in Form von Anomalien. Inkonsistenzen und Anomalien müssen jedoch möglichst früh im Entwurfsprozess erkannt und behoben werden, um drastische Folgekosten zur Laufzeit eines Systems zu vermeiden. Aus diesem Grund sind statische Analysetechniken zur automatisierten Analyse integrierter Software-Produktlinien-Spezifikationen unabdingbar.

Existierende Ansätze zur Konsistenzprüfung erfordern, dass der Suchraum für die Instanzsuche vorab entweder manuell oder durch heuristisch identifizierte Schranken eingeschränkt wird. Da, falls keine Instanz gefunden werden kann, nicht bekannt ist, ob dies durch einen zu klein gewählten Suchraum oder eine tatsächliche Inkonsistenz verursacht wurde, sind existierende Analyseverfahren inhärent unvollständig und praktisch nur eingeschränkt nutzbar. Darüber hinaus wurden bisher noch keine Analysen zur Identifikation von Anomalien vorgeschlagen, wie sie beispielsweise in Variabilitätsmodellen auftreten können. Weiterhin erlauben existierende Verfahren zwar die Handhabung von ganzzahligen Attributen, ermöglichen jedoch keine effiziente Analyse von Spezifikationen die zusätzlich reellwertige Attribute aufweisen.

In dieser Arbeit präsentieren wir einen Ansatz zur automatisierten Analyse integrierter Software-Produktlinien-Spezifikationen, die in der Sprache Clafer spezifiziert sind. Hierfür präsentieren wir eine ganzheitliche Spezifikation der strukturellen Konsistenzeigenschaften laufzeitadaptiver Software-Systeme und schlagen neuartige Anomalietypen vor, die in Clafer-Spezifikationen auftreten können. Wir charakterisieren eine Kernsprache, die eine vollständige und korrekte Analyse von Clafer-Spezifikationen ermöglicht. Wir führen zusätzlich eine neuartige semantische Repräsentation als mathematisches Optimierungsproblem ein, die über die Kernsprache hinaus eine effiziente Analyse praxisrelevanter Clafer-Spezifikationen ermöglicht und die Anwendung etablierter Standard-Lösungsverfahren erlaubt. Die Methoden und Techniken dieser Arbeit werden anhand eines durchgängigen Beispiels eines selbst-adaptiven Kommunikationssystems illustriert und prototypisch implementiert. Die experimentelle Evaluation zeigt die Effektivität unseres Analyseverfahrens sowie erhebliche Verbesserungen der Laufzeiteffizienz im Vergleich zu etablierten Verfahren.

Alternatives oder übersetztes Abstract:
Alternatives AbstractSprache

Emerging trends for digital transformations (e.g., Smart Factories, Internet of Things, Smart Grids) lead to new usage scenarios that require software systems being able to reconfigure themselves continuously to meet changing environmental conditions. Integrated software product line specifications allow for precisely describing consistency properties of such systems in a uniform representation. To this end, the specification language Clafer provides means for both characterizing structural run-time variability as well as specifying re-configurable elements of the system architecture and complex dependencies. For this purpose, Clafer combines UML-like class- and meta-modeling with feature-oriented variability modeling and first-order logic constraints. This considerable expressiveness leads to complex specifications in practice (e.g. due to hidden dependencies between configuration options and components of the system architecture). As a result, integrated software product line specifications tend to be prone to specification errors such as inconsistencies or anomalies (e.g., dead configuration options that can never be selected). However, inconsistencies and anomalies should be identified and rectified as early as possible in the development process to avoid critical system states and involved follow-up costs in case of system failures. For this reason, static analysis techniques for automated validation of integrated product line specifications are crucially needed.

Recent analysis techniques for checking model consistency of integrated product line specifications impose an a priori finite search space with either manually or heuristically adjusted bounds. However, these techniques are inherently incomplete thus yielding results for which it is unknown whether initially chosen bounds are sufficient and, therefore, have limited practical applicability. Furthermore, no techniques for automated anomaly detection in Clafer specifications that have been proposed so far go beyond inconsistency analysis and allow for identifying more sophisticated anomaly types (as e.g., dead multiplicity intervals). Moreover, existing approaches for consistency checking provide only limited support for analyzing specifications with complex integer attributes and almost no support for real-valued attributes.

In this thesis, we present an approach for automated analysis of integrated product line specifications that are specified in Clafer. To this end, we present a uniform specification of structural consistency properties of self-adaptive systems and lift existing notions of more sophisticated anomaly types to Clafer specifications. To tackle the completeness problem, we present a restricted, yet sufficiently expressive sublanguage of Clafer for which complete and correct consistency checks are feasible. Additionally, we introduce a novel semantic representation as a mathematical optimization problem enabling the efficient analysis of practically relevant specifications and allowing to apply well-established off-the-shelf solvers. The methods and techniques presented in this thesis are illustrated by means of a running example from the communication network domain. Furthermore, we provide a prototypical implementation of the presented approach. Our experimental evaluation shows remarkable improvements of run-time efficiency as well as effectiveness of anomaly detection as compared to existing techniques.

Englisch
URN: urn:nbn:de:tuda-tuprints-88750
Sachgruppe der Dewey Dezimalklassifikatin (DDC): 000 Allgemeines, Informatik, Informationswissenschaft > 004 Informatik
600 Technik, Medizin, angewandte Wissenschaften > 620 Ingenieurwissenschaften und Maschinenbau
Fachbereich(e)/-gebiet(e): 18 Fachbereich Elektrotechnik und Informationstechnik
18 Fachbereich Elektrotechnik und Informationstechnik > Institut für Datentechnik > Echtzeitsysteme
18 Fachbereich Elektrotechnik und Informationstechnik > Institut für Datentechnik
DFG-Sonderforschungsbereiche (inkl. Transregio)
DFG-Sonderforschungsbereiche (inkl. Transregio) > Sonderforschungsbereiche
DFG-Sonderforschungsbereiche (inkl. Transregio) > Sonderforschungsbereiche > SFB 1053: MAKI – Multi-Mechanismen-Adaption für das künftige Internet
DFG-Sonderforschungsbereiche (inkl. Transregio) > Sonderforschungsbereiche > SFB 1053: MAKI – Multi-Mechanismen-Adaption für das künftige Internet > A: Konstruktionsmethodik
DFG-Sonderforschungsbereiche (inkl. Transregio) > Sonderforschungsbereiche > SFB 1053: MAKI – Multi-Mechanismen-Adaption für das künftige Internet > A: Konstruktionsmethodik > Teilprojekt A4: Selbst-Adaption
Hinterlegungsdatum: 11 Aug 2019 19:55
Letzte Änderung: 21 Apr 2020 15:05
PPN:
Referenten: Schürr, Prof. Dr. Andreas ; Becker, Prof. Dr. Christian
Datum der mündlichen Prüfung / Verteidigung / mdl. Prüfung: 28 Juni 2019
Export:
Suche nach Titel in: TUfind oder in Google
Frage zum Eintrag Frage zum Eintrag

Optionen (nur für Redakteure)
Redaktionelle Details anzeigen Redaktionelle Details anzeigen