Abschlussvortrag: Konzeption und Implementierung der automatisierten formalen Analyse von erweiterten Feature-Modellen mittels Constraint-Programmierung sowie Satisfiability Modulo Theories in Glencoe

Betreuer: Professor Dr. Georg Rock

Kurzfassung:
Das Streben der Gesellschaft nach Selbstverwirklichung und Individualität wächst mit der heutigen Globalisierung der Märkte. Als Folge dieser Entwicklungen lassen sich unter anderem die steigende Relevanz der Individualisierung von Konsumgütern jeglicher Art benennen. Dies zeigt auch die schier unendliche Anzahl an Produktvarianten, welche durch die in den freien Märkten agierenden Unternehmen überblickt werden muss. In diesem Zusammenhang haben sich Feature-Modelle als bewährte Methodik zur Strukturierung derartiger Varianzinformationen durchgesetzt. Gründe hierfür sind neben ihrer Möglichkeit sie durch den Einsatz von SAT-Solvern formal zu analysieren, ihr hohes Maß an Verständlichkeit und eindeutige Semantik. Die Integration weiterer Charakteristiken, wie beispielsweise arithmetischer Ausdrücke, in ein Feature-Modell führt jedoch zu einem signifikanten Anstieg der Größe sowie Komplexität eines Modells. Die in sogenannten erweiterten Feature-Modellen enthaltenen Feature-Attribute stellen eine adäquate Lösung zur Abbildung derartiger Charakteristiken dar, verhindern jedoch die unmittelbare formale Analyse der Modelle durch SAT-Solver.

Aus diesem Grund thematisiert die hier vorliegende Arbeit die automatisierte formale Analyse erweiterter Feature-Modelle mittels Constraint-Programmierung sowie Satisfiability Modulo Theories. Dies umfasst zunächst eine formale Definition grundlegender Begrifflichkeiten der Feature-Modellierung, Constraint-Pro"-gram"-mie"-rung und Satisfiability Modulo Theories. Ebenso Teil dieser Arbeit ist die Vorstellung und Realisierung eines Konzeptes zur Visualisierung, Modellierung wie auch formalen Analyse erweiterter Feature-Modelle in der Webanwendung Glencoe. Diese automatisierte formale Analyse wird durch die Transformation der Modelle in ein CSP oder SMT-Problem sowie die Integration sogenannter CSP- und SMT-Solver ermöglicht. Derartige Solver erlauben zudem eine Optimierung der in einem Feature-Modell enthaltenen Produkte hinsichtlich spezifischer Charakteristiken innerhalb der Anwendung Glencoe.