Formal methods for the validation of automotive product configuration data
Formal methods for the validation of automotive product configuration data
复制标题
DOI：
10.1017/s0890060403171065
复制
发表时间：
2003-02
期刊：
影响因子：
--
通讯作者：
C. Sinz;Andreas Kaiser;W. Küchlin
中科院分区：
文献类型：
--
作者：
C. Sinz;Andreas Kaiser;W. Küchlin
在汽车行业中，编制和维护正确的产品配置数据是一项复杂的任务。我们的工作展示了如何将正式方法应用于此类业务关键数据的验证。我们的一致性支持工具BIS在现有的布尔约束数据库上工作，这些约束表示有效的配置及其到可制造产品的转换。使用带有解释组件的特别修改的可满足性检查器，BIS可以检测约束集合中的不一致，从而帮助提高产品数据的质量。BIS还通过计算产品或生产环境变化对所需部件集的影响来支持制造决策。在本文中，我们对BIS进行了全面的描述：其构建背后的业务流程的形式化，在此背景下我们发现有必要对可满足性检查技术进行修改，以及用于将产品打包为客户-服务器信息系统的软件技术。
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.