Hostname: page-component-78c5997874-dh8gc Total loading time: 0 Render date: 2024-11-17T16:15:13.897Z Has data issue: false hasContentIssue false
  • English
  • Français

Formal methods for the validation of automotive product configuration data

Published online by Cambridge University Press:  07 August 2003

CARSTEN SINZ ,
ANDREAS KAISER  and
WOLFGANG KÜCHLIN
CARSTEN SINZ
Affiliation:
WSI for Computer Science, Symbolic Computation Group, University of Tübingen and Steinbeis Technology Transfer Center OIT, Tübingen, Germany
ANDREAS KAISER
Affiliation:
WSI for Computer Science, Symbolic Computation Group, University of Tübingen and Steinbeis Technology Transfer Center OIT, Tübingen, Germany
WOLFGANG KÜCHLIN
Affiliation:
WSI for Computer Science, Symbolic Computation Group, University of Tübingen and Steinbeis Technology Transfer Center OIT, Tübingen, Germany
Get access Rights & Permissions [Opens in a new window]

Abstract

In the automotive industry, the compilation and maintenance of correct product configuration data is a complex task. Our work shows how formal methods can be applied to the validation of such business critical data. Our consistency support tool BIS works on an existing database of Boolean constraints expressing valid configurations and their transformation into manufacturable products. Using a specially modified satisfiability checker with an explanation component, BIS can detect inconsistencies in the constraints set and thus help increase the quality of the product data. BIS also supports manufacturing decisions by calculating the implications of product or production environment changes on the set of required parts. In this paper, we give a comprehensive account of BIS: the formalization of the business processes underlying its construction, the modifications of satisfiability-checking technology we found necessary in this context, and the software technology used to package the product as a client–server information system.

Type
Research Article
Information
AI EDAM , Volume 17 , Issue 1 , February 2003 , pp. 75 - 97
Copyright
© 2003 Cambridge University Press

Access options

Get access to the full version of this content by using one of the access options below. (Log in options will check for institutional or personal access. Content may require purchase if you do not have access.)

References

REFERENCES

Barker, V. & O'Connor, D. (1989). Expert systems for configuration at Digital: XCON and beyond. Communications of the ACM 32(3), 298–318.Google Scholar
Bayardo, R.J. & Schrag, R.C. (1997). Using CSP look-back techniques to solve real-world SAT instances. AAAI'97: Proc. Fourteenth National Conf. Artificial Intelligence.
Blochinger, W., Sinz, C., & Küchlin, W. (2001). Parallel consistency checking of automotive product data. Proc. Int. Conf. Parallel Computing (ParCo 2001), Naples, Italy.
CORBA. (1995). The Common Object Request Broker: Architecture and Specification. Needham, MA: Object Management Group.
Craigen, D., Gerhart, S., & Ralston, T. (1995). Formal methods reality check: Industrial usage. IEEE Transaction on Software Engineering 21(2), 90–98.Google Scholar
Davis, M., Logemann, G., & Loveland, D. (1962). A machine program for theorem-proving. Communications of the ACM 5, 394–397.Google Scholar
Davis, M. & Putnam, H. (1960). A computing procedure for quantification theory. Journal of the ACM 7, 201–215.Google Scholar
Davydov, D., Davydova, I., & Kleine Büning, H. (1998). An efficient algorithm for the minimal unsatisfiability problem for a subclass of CNF. Annals of Mathematics and Artificial Intelligence 23, 229–245.Google Scholar
Freuder, E. (1998). The role of configuration knowledge in the business process. IEEE Intelligent Systems 13(4), 29–31.Google Scholar
Gerhart, S. (1990). Applications of formal methods: Developing virtuoso software. IEEE Software 7(5), 7–10.Google Scholar
Günter, A. & Kühn, C. (1999). Knowledge-based configuration: Survey and future directions. LNAI 1570, 47–66.Google Scholar
Haag, A. (1998). Sales configuration in business processes. IEEE Intelligent Systems 13(4), 78–85.Google Scholar
Hall, A. (1990). Seven myths of formal methods. IEEE Software 7(5), 11–19.Google Scholar
Hooker, J. & Vinay, V. (1995). Branching rules for satisfiability. Journal of Automated Reasoning 15(3), 359–383.Google Scholar
Kaiser, A. (2001). A SAT-based Propositional Prover for Consistency Checking of Automotive Product Data. Technical Report WSI-2001-16. Tübingen, Germany: Wilhelm-Schickard-Institut für Informatik, Eberhard-Karls-Universität Tübingen.
Kaiser, A. & Küchlin, W. (2001a). Detecting inadmissible and necessary variables in large propositional formulae. Proc. Intl. Joint Conf. Automated Reasoning: IJCAR 2001—Short Papers, pp. 96–102. Technical Report DII, 11/01. University of Siena.
Kaiser, A. & Küchlin, W. (2001b). Explaining inconsistencies in combinatorial automotive product data. Proc. 2nd Int. Conf. Intelligent Technologies (InTech 2001), pp. 198–204. Assumption University, Bangkok, Thailand.
Kleine Büning, H. & Xishun, Z. (1998). On the structure of some classes of minimal unsatisfiable formulas. Proc. 5th Int. Symp. Artificial Intelligence and Mathematics, Fort Lauderdale, FL.
Küchlin, W. & Sinz, C. (2000). Proving consistency assertions for automotive product data management. Journal of Automated Reasoning 24(1–2), 145–163.Google Scholar
Kullmann, O. (2000). An application of matroid theory to the SAT problem. Proc. 15th IEEE Conf. Computational Complexity—CCC 2000, pp. 116–124, Florence, Italy.
McDermott, J. (1982). R1: A rule-based configurer of computer systems. Artificial Intelligence 19(1), 39–88.Google Scholar
Moskewicz, M., Madigan, C., Zhao, Y., Zhang, L., & Malik, S. (2001). Chaff: Engineering an efficient SAT solver. Proc. 38th Design Automation Conf. (DAC 2001), pp. 530–535. New York: ACM.
Papadimitriou, C.H. & Wolfe, D. (1988). The complexity of facets resolved. Journal of Computer and System Sciences 37, 2–13.Google Scholar
Robinson, J.A. (1965). A machine-oriented logic based on the resolution principle. Journal of the ACM 12, 23–41.Google Scholar
Sabin, D. & Weigel, R. (1998). Product configuration frameworks—A survey. IEEE Intelligent Systems 13(4), 42–49.Google Scholar
Saiedian, H. (1996). An invitation to formal methods. IEEE Computer 29(4), 16–17.Google Scholar
Silva, J.P.M. & Sakallah, K.A. (1999). GRASP—A new search algorithm for satisfiability. IEEE Transactions on Computers 48(5), 506–521.Google Scholar
Sinz, C. (1997). Baubarkeitsprüfung von Kraftfahrzeugen durch automatisches Beweisen. Diplomarbeit, Universität Tübingen.
Sinz, C. & Küchlin, W. (2001). Dealing with temporal change in product documentation for manufacturing. Configuration Workshop Proc., 17th Int. Joint Conf. Artificial Intelligence (IJCAI-2001), pp. 71–77, Seattle, WA.
Soininen, T., Niemelä, I., Tiihonen, J., & Sulonen, R. (2001). Representing configuration knowledge with weight constraint rules. Answer Set Programming: Towards Efficient and Scalable Knowledge Representation and Reasoning, 2001 AAAI Spring Symposium, pp. 195–201. Menlo Park, CA: AAAI Press.
Somenzi, F. (1998). CUDD: CU Decision Diagram Package, Release 2.3.0. University of Colorado, Boulder. Available online at http://vlsi.colorado.edu/∼fabio.
Timmermans, P. (1999). The business challenge of configuration. In Configuration (Faltings, B., Freuder, E., Friedrich, G. & Felfernig, A., Eds.), pp. 119–122. Workshop Technical Report WS-99-05. Menlo Park, CA: AAAI Press.
Tseitin, G.S. (1970). On the complexity of derivation in propositional calculus. In Studies in Constructive Mathematics and Mathematical Logic (Silenko, A.O., Ed.), pp. 115–125. Leningrad: V.A. Steklov Mathematical Institute.
Waldinger, R.J. & Stickel, M.E. (1992). Proving properties of rule based systems. International Journal of Software Engineering and Knowledge Engineering 2(1), 121–144.Google Scholar
Wing, J. (1990). A specifier's introduction to formal methods. IEEE Computer 23(9), 8–24.Google Scholar
Wing, J. & Woodcock, J. (2000). Special issues for FM'99: The First World Congress on Formal Methods in the Development of Computing Systems. IEEE Transactions in Software Engineering 26(8), 673–674.Google Scholar
Wright, J.R., Weixelbaum, E., Vesonder, G.T., Brown, K.E., Palmer, S.R., Berman, J.I., & Moore, H.H. (1993). A knowledge-based configurator that supports sales, engineering, and manufacturing at AT&T Network Systems. AI Magazine 14(3), 69–80.Google Scholar
Zhang, H. (1997). SATO: An efficient propositional prover. Proc. 14th Int. Conf. on Automated Deduction (CADE-97), pp. 272–275. Lecture Notes in Computer Science, No. 1249. New York: Springer–Verlag.