TOBIAS-lib - Verifikation regelbasierter Konfigurationssysteme

Lizenz / license
Bitte zitieren sie dieses Dokument als / Please cite this document using URN: urn:nbn:de:bsz:21-opus-10550 URL: http://w210.ub.uni-tuebingen.de/dbt/volltexte/2004/1055/	Documents hosted by TOBIAS-lib

Sinz, Carsten

Verifikation regelbasierter Konfigurationssysteme

pdf-Format:

Dokument 1.pdf (3,514 KB)

Gedruckte Ausgabe:
Print-on-Demand-Kopie

Verification of rule-based configuration systems

Kurzfassung in deutsch
Komplexe Produkte wie z.B. Kraftfahrzeuge können in einer Vielzahl von
Varianten bestellt werden. Nicht jede gewünschte Konfiguration ist aber
tatsächlich realisierbar, da verschiedenste Rahmenbedingungen (geometrische,
funktionale, vertriebsbedingte, länderspezifische) eingehalten werden müssen.
Daher werden in der Praxis Konfigurationssysteme eingesetzt, die eine
automatisierte Verwaltung der Einschränkungen und der Produktvarianten
ermöglichen.

In dieser Arbeit wird die Anwendbarkeit formaler Methoden zur
Konsistenzprüfung (Verifikation) solcher Konfigurationssysteme untersucht.
Neben der ausführlichen Darstellung der Grundlagen - einschließlich einem
Vergleich verschiedener Formalismen - ist insbesondere die Evaluierung der
vorgeschlagenen Methoden anhand des Konfigurationssystems DIALOG von
DaimlerChrysler wesentlicher Bestandteil der Arbeit.

Verschiedene Korrektheitskriterien werden formuliert. Diese werden
zusammen mit dem gesamten Auftragsbearbeitungsprozess in dynamischer
Aussagenlogik (PDL) codiert und dadurch automatischen Beweisverfahren
zugänglich gemacht. Anstelle einer direkten Generierung der Beweise in PDL
wird ein Verfahren vorgeschlagen, das auf einer Transformation von PDL nach
Aussagenlogik beruht. Dadurch wird der Einsatz moderner SAT-Checker ermöglicht.

Insgesamt können so Gesamtaussagen über alle möglichen gültigen
Produktkonfigurationen formuliert und bewiesen werden, die ansonsten nicht
möglich wären. Fehler bei der Bearbeitung von Aufträgen lassen sich damit
letztendlich reduzieren.

Kurzfassung in englisch
Complex products like motor vehicles can be ordered by the customer
in a great number of variations. It may turn out, however, that an ordered
configuration is not actually manufacturable. Geometrical, functional, country
specific, and sales restrictions have to be considered.
Therefore, electronic configuration systems are employed, allowing an
automatized management of both product variants and constraints.

In our work we examine how to apply formal methods to check consistency
of such configuration systems. We give a thorough introduction to
configuration systems - including a comparison of different formalisms - and
demonstrate the feasibility of our verification approach by applying it to
the DIALOG system which is used by DaimlerChrysler to configure their
Mercedes car and truck lines.

We formulate different consistency properties and encode them - together
with the whole order management process - in propositional dynamic logic (PDL).
Thus, we enable the use of automatic theorem proving methods.
Instead of generating proofs in PDL directly, we propose a translation
of PDL proof obligations to purely propositional logic assertions.
That way we can make use of advanced SAT-checking methods.

Our approach allows to formulate assertions about the totality of all valid
product instances. Errors in the product data base - and ultimately in the
order management process - may thus be reduced.

SWD-Schlagwörter: Verifikation , Konfigurationsprüfung , Konfiguration <Informatik> , Automatisches Beweisverfahren , Dynamische Logik

Freie Schlagwörter (englisch): verification , product configuration , automatic theorem proving , propositional dynamic logic

Institut: Bereich 17 Fakultät für Informations- und Kognitionswissenschaften

Fakultät: 17 Fakultät für Informations- und Kognitionswissenschaften

DDC-Sachgruppe: Informatik

Dokumentart: Dissertation

Hauptberichter: Küchlin, Wolfgang

Sprache: deutsch

Tag der mündlichen Prüfung: 17.12.2003

Erstellungsjahr: 2003

Publikationsdatum: 21.01.2004

Lizenz: Veröffentlichungsvertrag

Gedruckte Ausgabe: Print-on-Demand-Kopie

Verification of rule-based configuration systems Kurzfassung in deutsch Komplexe Produkte wie z.B. Kraftfahrzeuge können in einer Vielzahl von Varianten bestellt werden. Nicht jede gewünschte Konfiguration ist aber tatsächlich realisierbar, da verschiedenste Rahmenbedingungen (geometrische, funktionale, vertriebsbedingte, länderspezifische) eingehalten werden müssen. Daher werden in der Praxis Konfigurationssysteme eingesetzt, die eine automatisierte Verwaltung der Einschränkungen und der Produktvarianten ermöglichen. In dieser Arbeit wird die Anwendbarkeit formaler Methoden zur Konsistenzprüfung (Verifikation) solcher Konfigurationssysteme untersucht. Neben der ausführlichen Darstellung der Grundlagen - einschließlich einem Vergleich verschiedener Formalismen - ist insbesondere die Evaluierung der vorgeschlagenen Methoden anhand des Konfigurationssystems DIALOG von DaimlerChrysler wesentlicher Bestandteil der Arbeit. Verschiedene Korrektheitskriterien werden formuliert. Diese werden zusammen mit dem gesamten Auftragsbearbeitungsprozess in dynamischer Aussagenlogik (PDL) codiert und dadurch automatischen Beweisverfahren zugänglich gemacht. Anstelle einer direkten Generierung der Beweise in PDL wird ein Verfahren vorgeschlagen, das auf einer Transformation von PDL nach Aussagenlogik beruht. Dadurch wird der Einsatz moderner SAT-Checker ermöglicht. Insgesamt können so Gesamtaussagen über alle möglichen gültigen Produktkonfigurationen formuliert und bewiesen werden, die ansonsten nicht möglich wären. Fehler bei der Bearbeitung von Aufträgen lassen sich damit letztendlich reduzieren. Kurzfassung in englisch Complex products like motor vehicles can be ordered by the customer in a great number of variations. It may turn out, however, that an ordered configuration is not actually manufacturable. Geometrical, functional, country specific, and sales restrictions have to be considered. Therefore, electronic configuration systems are employed, allowing an automatized management of both product variants and constraints. In our work we examine how to apply formal methods to check consistency of such configuration systems. We give a thorough introduction to configuration systems - including a comparison of different formalisms - and demonstrate the feasibility of our verification approach by applying it to the DIALOG system which is used by DaimlerChrysler to configure their Mercedes car and truck lines. We formulate different consistency properties and encode them - together with the whole order management process - in propositional dynamic logic (PDL). Thus, we enable the use of automatic theorem proving methods. Instead of generating proofs in PDL directly, we propose a translation of PDL proof obligations to purely propositional logic assertions. That way we can make use of advanced SAT-checking methods. Our approach allows to formulate assertions about the totality of all valid product instances. Errors in the product data base - and ultimately in the order management process - may thus be reduced.
SWD-Schlagwörter:		Verifikation , Konfigurationsprüfung , Konfiguration <Informatik> , Automatisches Beweisverfahren , Dynamische Logik
Freie Schlagwörter (englisch):		verification , product configuration , automatic theorem proving , propositional dynamic logic
Institut:		Bereich 17 Fakultät für Informations- und Kognitionswissenschaften
Fakultät:		17 Fakultät für Informations- und Kognitionswissenschaften
DDC-Sachgruppe:		Informatik
Dokumentart:		Dissertation
Hauptberichter:		Küchlin, Wolfgang
Sprache:		deutsch
Tag der mündlichen Prüfung:		17.12.2003
Erstellungsjahr:		2003
Publikationsdatum:		21.01.2004
Lizenz:		Veröffentlichungsvertrag
Gedruckte Ausgabe:		Print-on-Demand-Kopie


	Home \| Hilfe \| Kontakt \| Index \| Policy \| Disclaimer \| Impressum

Fragen, Anregungen, Feedback Universitätsbibliothek, TOBIAS-lib, Tel. +49 (0)7071/29-76999 Wilhelmstr. 32, 72016 Tübingen, H232, 235, 236