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 Model Translator
- 4.5 KConfigReader
- 4.6 Zusammenfassung
- 5 Fazit
Zielsetzung und Themenschwerpunkte
Diese Seminararbeit befasst sich mit der Übersetzung von Variabilitätsmodellen in aussagenlogische Formeln. Das Ziel ist es, die verschiedenen Werkzeuge und Algorithmen zu vergleichen, die diese Aufgabe erfüllen, und ihre Stärken und Schwächen aufzuzeigen. Der Fokus liegt dabei auf der Analyse der Korrektheit der Übersetzungen, der Redundanz in den Ergebnissen und dem Umgang mit nicht-booleschen Elementen.
- Vergleich von Werkzeugen und Algorithmen zur Übersetzung von Variabilitätsmodellen in aussagenlogische Formeln
- Analyse der Korrektheit und Effizienz der Übersetzungen
- Bewertung des Umgangs mit nicht-booleschen Elementen
- Untersuchung der Redundanz in den Ergebnissen
- Anwendungen der Übersetzung in der Praxis
Zusammenfassung der Kapitel
Kapitel 1 führt die Fragestellung der Arbeit ein und erläutert die Motivation und die Ziele des Surveys. Kapitel 2 bietet eine Einführung in die Grundlagen der Software-Produktlinienentwicklung, insbesondere das Variabilitätsmodell von Linux und die Verwendung von KConfig. Kapitel 3 behandelt die notwendigen Grundlagen der Aussagenlogik, die Übersetzung von Variabilitätsmodellen in aussagenlogische Formeln und das DIMACS Format. Kapitel 4 stellt die verschiedenen Werkzeuge und Algorithmen vor, die KConfig-Modelle in das CNF beziehungsweise DIMACS Format übersetzen können, und analysiert ihre Eigenschaften. Kapitel 5 fasst die Ergebnisse zusammen und zieht ein Fazit.
Schlüsselwörter
Variabilitätsmodelle, Aussagenlogik, CNF, DIMACS, KConfig, Software-Produktlinienentwicklung, Werkzeugvergleich, Übersetzung, Erfüllbarkeitsprobleme, SAT-Solver.
- Citation du texte
- Lea Kristin Gerling (Auteur), 2015, Werkzeuggestützte Ableitung Boolescher Modelle auf Grundlage existierender Variabilitätsmodelle. Eine Betrachtung, Munich, GRIN Verlag, https://www.grin.com/document/335400
