New Formal Methods for Automotive Configuration

Abstract

Die Komplexität der Automobilkonfiguration hat in den letzten Jahrzehnten extrem zugenommen. Ein typischer deutscher Premiumhersteller kann bis zu 10^80 Varianten eines einzigen Fahrzeugmodells bauen. Dieser Variantenreichtum muss jedoch entlang der gesamten Prozesskette—vom Produktentstehungsprozess bis hin zur Fertigung im Werk—verwaltet und beherrscht werden. Hierzu müssen von Experten einerseits die vom Kunden bestellbaren Fahrzeuge dokumentiert werden (High Level Regelwerk), andererseits müssen diesen Fahrzeugen physikalische Teile, Steuergeräte und Softwarekonfigurationen zugeordnet werden (Low Level Regelwerk). Die vorliegende Arbeit führt einen neuen generischen Formalismus für Konfigurationsdaten in der Automobilindustrie ein und präsentiert einen ausführlichen Überblick über die in der Industrie vorkommenden Prüfmöglichkeiten. In verschiedenen Industriekooperationen mit z.B. Audi, BMW, Daimler, Opel und VW wurde verifiziert, dass dieser Formalismus auf diese Hersteller übertragbar ist. Viele der bestehenden Prüfalgorithmen werden in dieser Dissertation entscheidend optimiert und werden im Rahmen des neuen generischen Frameworks formuliert. Es werden neue Prüf- und Analysemöglichkeiten auf Konfigurationsdaten vorgestellt. Dies sind unter anderem das Zählen baubarer Fahrzeuge, die Berechnung minimaler und maximaler Kundenorders oder die Berechnung von direkten Zwängen in der Konfigurationsbasis. Ein Hauptbeitrag dieser Arbeit ist die Einführung der Booleschen Quantorenelimination in der Automobilkonfiguration. Während die Quantorenelimination bisher vor allem im Bereich des symbolischen Modelcheckings zu finden war, werden hier zwei Anwendungen in der Automobilindustrie identifiziert, die großes Interesse in den industriellen Kooperationen erweckt haben. Es werden verschiedene Ansätze zur Booleschen Quantorenelimination vorgestellt und bezüglich der Anwendungen evaluiert. Im Rahmen dieser Arbeit entstand die Softwarebibliothek AutoLib, die die vorgestellten Algorithmen implementiert und vor allem einen neuen SAT Solver mit sich bringt, der sowohl Inkrementalität und Dekrementalität, als auch das sogenannte Proof Tracing, also das Aufzeichnen von Beweisen bei Nicht-Erfüllbarkeit, implementiert. Nach unserem Wissen ist dies der einzige SAT Solver, der diese beiden Funktionen auch in Kombination unterstützt. AutoLib wird aktuell in einem Produktivsystem bei BMW sowie in Prototypen bei Audi/VW und bei Daimler eingesetzt. Alle Algorithmen, die in dieser Arbeit präsentiert werden, wurden in einer Mach- barkeitsstudie bei BMW in den Jahren 2012 und 2013 implementiert und auf ihre industrielle Einsetzbarkeit hin verifiziert. Ein Produktivsystem, das Teile dieser Algorithmen umfasst und auf AutoLib basiert, hatte im Mai 2014 GoLive bei BMW.