CPL - Chalmers Publication Library
| Utbildning | Forskning | Styrkeområden | Om Chalmers | In English In English Ej inloggad.

On Formal Methods for Large-Scale Product Configuration

Alexey Voronov (Institutionen för signaler och system, Automation)
Göteborg : Chalmers University of Technology, 2013. ISBN: 978-91-7385-790-1.- 192 s.
[Doktorsavhandling]

In product development companies mass customization is widely used to achieve better customer satisfaction while keeping costs down. To efficiently implement mass customization, product platforms are often used. A product platform allows building a wide range of products from a set of predefined components. The process of matching these components to customers' needs is called product configuration. Not all components can be combined with each other due to restrictions of various kinds, for example, geometrical, marketing and legal reasons. Product design engineers develop configuration constraints to describe such restrictions. The number of constraints and the complexity of the relations between them are immense for complex product like a vehicle. Thus, it is both error-prone and time consuming to analyze, author and verify the constraints manually. Software tools based on formal methods can help engineers to avoid making errors when working with configuration constraints, thus design a correct product faster.

This thesis introduces a number of formal methods to help engineers maintain, verify and analyze product configuration constraints. These methods provide automatic verification of constraints and computational support for analyzing and refactoring constraints. The methods also allow verifying the correctness of one specific type of constraints, item usage rules, for sets of mutually-exclusive required items, and automatic verification of equivalence of different formulations of the constraints. The thesis also introduces three methods for efficient enumeration of valid partial configurations, with benchmarking of the methods on an industrial dataset.

Handling large-scale industrial product configuration problems demands high efficiency from the software methods. This thesis investigates a number of search-based and knowledge-compilation-based methods for working with large product configuration instances, including Boolean satisfiability solvers, binary decision diagrams and decomposable negation normal form. This thesis also proposes a novel method based on supervisory control theory for efficient reasoning about product configuration data. The methods were implemented in a tool, to investigate the applicability of the methods for handling large product configuration problems. It was found that search-based Boolean satisfiability solvers with incremental capabilities are well suited for industrial configuration problems.

The methods proposed in this thesis exhibit good performance on practical configuration problems, and have a potential to be implemented in industry to support product design engineers in creating and maintaining configuration constraints, and speed up the development of product platforms and new products.

Nyckelord: product configuration, constraint satisfaction, Boolean satisfiability, knowledge compilation, supervisory control theory



Den här publikationen ingår i följande styrkeområden:

Läs mer om Chalmers styrkeområden  

Denna post skapades 2012-12-19. Senast ändrad 2013-09-25.
CPL Pubid: 168379

 

Läs direkt!

Lokal fulltext (fritt tillgänglig)


Institutioner (Chalmers)

Institutionen för signaler och system, Automation

Ämnesområden

Informations- och kommunikationsteknik
Produktion
Datavetenskap (datalogi)
Systemvetenskap, informationssystem och informatik
Elektroteknik och elektronik
Farkostteknik

Chalmers infrastruktur

Relaterade publikationer

Inkluderade delarbeten:


SAT-Solving in Practice, with a Tutorial Example from Supervisory Control


Enumeration of valid partial configurations


Verification of Item Usage Rules in Product Configuration


Examination

Datum: 2013-01-18
Tid: 10:00
Lokal: EA
Opponent: Dr. rer. nat. Carsten Sinz, Institute for Theoretical Computer Science, Karlsruhe Institute of Technology, Germany

Ingår i serie

Doktorsavhandlingar vid Chalmers tekniska högskola. Ny serie 0346-718X