Abstract:
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.