Verifikation regelbasierter Konfigurationssysteme

Abstract

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.

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.