New Formal Methods for Automotive Configuration

DSpace Repository

Show simple item record

dc.contributor.advisor Küchlin, Wolfgang (Prof. Dr.)
dc.contributor.author Zengler, Christoph
dc.date.accessioned 2014-10-28T09:16:14Z
dc.date.available 2014-10-28T09:16:14Z
dc.date.issued 2014
dc.identifier.other 416167454 de_DE
dc.identifier.uri http://hdl.handle.net/10900/57198
dc.identifier.uri http://nbn-resolving.de/urn:nbn:de:bsz:21-dspace-571984 de_DE
dc.description.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. de_DE
dc.language.iso en de_DE
dc.publisher Universität Tübingen de_DE
dc.rights ubt-podok de_DE
dc.rights.uri http://tobias-lib.uni-tuebingen.de/doku/lic_mit_pod.php?la=de de_DE
dc.rights.uri http://tobias-lib.uni-tuebingen.de/doku/lic_mit_pod.php?la=en en
dc.subject.classification Verifikation , Konfigurationsprüfung , Konfiguration <Informatik> , Automatisches Beweisverfahren , Erfüllbarkeitsproblem de_DE
dc.subject.ddc 004 de_DE
dc.subject.other verification en
dc.subject.other product configuration en
dc.subject.other automatic theorem proving en
dc.subject.other satisfiability problem en
dc.title New Formal Methods for Automotive Configuration en
dc.type PhDThesis de_DE
dcterms.dateAccepted 2014-10-17
utue.publikation.fachbereich Informatik de_DE
utue.publikation.fakultaet 7 Mathematisch-Naturwissenschaftliche Fakultät de_DE

Dateien:

This item appears in the following Collection(s)

Show simple item record