Es existieren verschiedene Werkzeuge und Algorithmen, die Variabilitätsmodelle in aussagenlogische Formeln übersetzen können. Diese Formeln können dann mithilfe von SAT-Solvern auf ihre Erfüllbarkeit überprüft werden. Als Anwendungsbeispiel dient das Variabilitätsmodell des Linux Kernels, das durch Verwendung von KConfig Dateien definiert und konfiguriert werden kann.
Diese Arbeit vergleicht die vorhandenen Werkzeuge und Algorithmen, die KConfig-Modelle in das DIMACS oder CNF Format übersetzen. Der Vergleich basiert dabei auf der vorhandenen Literatur. Dabei wird insbesondere darauf eingegangen, ob die erstellten Übersetzungen überhaupt korrekt sind, ob redundante Daten erzeugt werden und wie die Werkzeuge und Algorithmen mit nicht-Boolesche Elemente umgehen.
Inhaltsverzeichnis
1 Einleitung
1.1 Motivation und Ziele der Arbeit
1.2 Gliederung
2 Grundlagen der Software-Produktlinienentwicklung
2.1 Grundbegriffe
2.2 Das Linux Variabilitätsmodell
2.3 KConfig
3 Grundlagen der Aussagenlogik
3.1 Variabilitätsmodelle in Aussagenlogik übersetzen
3.2 Syntax und Semantik der Aussagenlogik
3.3 CNF und DIMACS
4 Vorstellung und Bewertung der Werkzeuge
4.1 LVAT
4.2 Tübinger Algorithmus
4.3 Undertaker
4.4 KConfig ModelTranslator
4.5 KConfigReader
4.6 Zusammenfassung
5 Fazit
Zielsetzung & Themen
Die Arbeit untersucht, wie Variabilitätsmodelle von Software-Produktlinien – mit dem Linux Kernel als zentralem Anwendungsbeispiel – in aussagenlogische Formeln überführt werden können, um diese mittels SAT-Solvern auf Validität und Konsistenz zu prüfen. Das primäre Ziel ist ein strukturierter Vergleich bestehender Werkzeuge und Algorithmen hinsichtlich ihrer Vorgehensweise, Ergebnisqualität und Handhabung komplexer Modellierungselemente.
- Grundlagen der Software-Produktlinienentwicklung und KConfig-Modellierung
- Methodik der Übersetzung von Variabilitätsmodellen in Aussagenlogik
- Vorstellung und Analyse der Werkzeuge (LVAT, Tübinger Algorithmus, Undertaker, KConfig ModelTranslator, KConfigReader)
- Umgang mit nicht-booleschen Elementen und Konsistenzprüfungen
- Eignung der Formate CNF und DIMACS für automatisierte Analysen
Auszug aus dem Buch
3.2 Syntax und Semantik der Aussagenlogik
Der folgende Abschnitt bietet eine kurze Einführung in die Grundlagen der Aussagenlogik. Dies hilft dabei, das Vorgehen der Werkzeuge aus Kapitel 4 besser verstehen zu können. Als Grundlage für die Erklärung von Syntax und Semantik der Aussagenlogik dient dabei die Überführung des Feature Modells einer Seminararbeit aus Abschnitt 2.1 und Abschnitt 2.3.
Die Aussagenlogik ist ein Teilgebiet der Logik. Mit ihrer Hilfe lässt sich der Wahrheitswert einer Aussage bestimmen [Rus10, S. 243]. Dieser ist entweder 1 oder 0 beziehungsweise wahr oder falsch. Eine Aussage ist beispielsweise der Satz „Eine Seminararbeit besitzt Inhalt“. Diese Aussage ist wahr. In der Aussagenlogik können auch mehrere Aussagen miteinander verknüpft werden, beispielsweise „Eine Seminararbeit besitzt Inhalt und auf dem Deckblatt steht die Art des Themas.“ Hier wurden zwei Aussagen mit einem logischen und verknüpft. Dadurch wird die Gesamtaussage nur wahr, wenn auch beide Teilaussagen wahr sind. Dies ist in dem Beispiel der Fall.
Insgesamt gibt es in der Aussagenlogik fünf verschiedene logische Verknüpfungen [Rus10, S. 244], die nachfolgend kurz erläutert werden. Dazu ist noch festzuhalten, dass es durchaus abweichende Schreibweisen gibt, in dieser Seminararbeit aber nur die nachfolgenden verwendet werden:
Zusammenfassung der Kapitel
1 Einleitung: Diese Einleitung motiviert die Fragestellung der Arbeit und erläutert die Zielsetzung sowie den inhaltlichen Aufbau der Seminararbeit.
2 Grundlagen der Software-Produktlinienentwicklung: Hier werden die Basiskonzepte der Produktlinienentwicklung eingeführt und das Variabilitätsmodell von Linux sowie die Sprache KConfig als Anwendungsbeispiel beschrieben.
3 Grundlagen der Aussagenlogik: Dieses Kapitel motiviert die Nutzung aussagenlogischer Formeln für Variabilitätsmodelle, führt in deren Syntax und Semantik ein und erläutert die Zielformate CNF und DIMACS.
4 Vorstellung und Bewertung der Werkzeuge: Der Hauptteil der Arbeit analysiert verschiedene Werkzeuge und Algorithmen zur Übersetzung von KConfig-Modellen in logische Formeln und vergleicht deren Arbeitsweisen.
5 Fazit: Das Fazit reflektiert die Erfüllung der Zielsetzung und diskutiert die gewonnenen Erkenntnisse über die Werkzeuge sowie den Bedarf für zukünftige Entwicklungen.
Schlüsselwörter
Software-Produktlinien, Variabilitätsmodell, KConfig, Aussagenlogik, SAT-Solver, DIMACS, CNF, Linux Kernel, Feature Modellierung, Konsistenzprüfung, LVAT, Undertaker, Modelltransformation, Software-Qualität, Formale Semantik.
Häufig gestellte Fragen
Worum geht es in dieser Arbeit grundsätzlich?
Die Arbeit bietet einen Überblick über Methoden und Werkzeuge, mit denen Variabilitätsmodelle von hochkonfigurierbaren Systemen (insb. Linux) in aussagenlogische Formeln übersetzt werden können, um automatisierte Analysen zu ermöglichen.
Was sind die zentralen Themenfelder?
Die Schwerpunkte liegen auf der Software-Produktlinienentwicklung, der formalen Modellierung mit KConfig, den Grundlagen der Aussagenlogik sowie der funktionalen Analyse spezifischer Analyse-Werkzeuge.
Was ist das primäre Ziel der Untersuchung?
Das Ziel ist es, dem Leser durch einen fundierten Vergleich bestehender Werkzeuge eine Entscheidungshilfe für die Auswahl geeigneter Algorithmen zur automatisierten Konfigurationsanalyse zu geben.
Welche wissenschaftliche Methode wird verwendet?
Es handelt sich um einen Survey, bei dem auf Basis vorhandener wissenschaftlicher Literatur und Werkzeugdokumentationen eine qualitative Analyse und ein strukturierter Vergleich der jeweiligen Vorgehensweisen durchgeführt werden.
Was wird im Hauptteil der Arbeit behandelt?
Der Hauptteil widmet sich detailliert der Vorstellung einzelner Werkzeuge wie LVAT, dem Tübinger Algorithmus, Undertaker, dem KConfig ModelTranslator und dem KConfigReader inklusive ihrer jeweiligen Prozessketten.
Welche Schlüsselbegriffe charakterisieren die Arbeit?
Die Arbeit wird maßgeblich durch Begriffe wie Variabilitätsmanagement, KConfig, SAT-Solver, Konsistenzanalyse und formale Methoden in der Softwareentwicklung definiert.
Warum ist die Übersetzung in das DIMACS-Format notwendig?
DIMACS dient als einheitliches, maschinenlesbares Eingabeformat für SAT-Solver, welche benötigt werden, um die logischen Formeln der Variabilitätsmodelle automatisiert auf Validität zu prüfen.
Wie gehen die untersuchten Werkzeuge mit nicht-booleschen Features um?
Die meisten Werkzeuge transformieren nicht-boolesche Features (wie int, string oder tristate) durch die Erstellung zusätzlicher boolescher Variablen und spezieller Constraints, um sie für SAT-Solver verarbeitbar zu machen.
- Quote paper
- Lea Kristin Gerling (Author), 2015, Werkzeuggestützte Ableitung Boolescher Modelle auf Grundlage existierender Variabilitätsmodelle. Eine Betrachtung, Munich, GRIN Verlag, https://www.grin.com/document/335400
