Proving Consistency Assertions for Automotive Product Data Management

We present a formal specification and verification approach for industrial product data bases containing Boolean logic formulae to express constraints. Within this framework, global consistency assertions about the product data are converted into propositional satisfiability problems. Today"s state-of-the-art provers turn out to be surprisingly efficient in solving the SAT-instances generated by this process. Moreover, we introduce a method for encoding special nonmonotonic constructs in traditional Boolean logic. We have successfully applied our method to industrial automotive product data management and could establish a set of commercially used interactive tools that facilitate the management of change and help raise quality standards.