Proving consistency assertions for automotive product data management

被引:24
作者
Küchlin, W
Sinz, C
机构
[1] Univ Tubingen, WSI Comp Sci, Symbol Computat Grp, D-72076 Tubingen, Germany
[2] Steinbeis Technol Transfer Ctr OIT, D-72076 Tubingen, Germany
关键词
formal specification; verification; product data management; product configuration; industrial application;
D O I
10.1023/A:1006370506164
中图分类号
TP18 [人工智能理论];
学科分类号
081104 ; 0812 ; 0835 ; 1405 ;
摘要
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.
引用
收藏
页码:145 / 163
页数:19
相关论文
共 22 条
  • [1] AKERS SB, 1978, IEEE T COMPUT, V27, P509, DOI 10.1109/TC.1978.1675141
  • [2] BORALV A, 1997, LECT NOTES COMPUT SC, V1554, P7
  • [3] BOWEN JP, 1994, LNCS, V873, P105
  • [4] BRYANT RE, 1986, IEEE T COMPUT, V35, P677, DOI 10.1109/TC.1986.1676819
  • [5] A COMPUTING PROCEDURE FOR QUANTIFICATION THEORY
    DAVIS, M
    PUTNAM, H
    [J]. JOURNAL OF THE ACM, 1960, 7 (03) : 201 - 215
  • [6] A MACHINE PROGRAM FOR THEOREM-PROVING
    DAVIS, M
    LOGEMANN, G
    LOVELAND, D
    [J]. COMMUNICATIONS OF THE ACM, 1962, 5 (07) : 394 - 397
  • [7] DERSHOWITZ N, 1990, FORMAL MODELS SEMANT, V2, pCH6
  • [8] Freeman J. W., 1995, Improvements to Propositional Satisfiability Search Algorithms
  • [9] GESER A, 1997, RISC LINZ REPORT SER
  • [10] HSIANG J, 1982, THESIS U ILLINOIS UR