@misc{8747,
  keywords = {Workshop},
  author = {Razieh Behjati and Shiva Nejati},
  title = {Interactive Configuration Verification Using Constraint Programming},
  abstract = {Configuration is a recurring problem in many domains. Manual configuration - the common practice in many companies - is time-consuming and error-prone, especially for large-scale systems. During the last three decades, researchers have developed a large number of approaches to automate various configuration use cases. Most of these approaches concern consistency of configuration decisions, and rely on CP or SAT solvers for ensuring consistency. We focus on interactive architecture-level configuration of Cyber-Physical Systems (CPS). In this context, engineers configure products by assigning values to tens of thousands of parameters. Typically, 15 to 20 percent of these parameters are interdependent. Finding consistent values for interdependent parameters without any automated support is challenging. In our interactive configuration approach, we map a configuration problem into a constraint network. During configuration, new variables or constraints may be added to the constraint network. We call this the dynamic growth of the constraint network. To ensure the consistency of configuration decisions, we use constraint propagation over finite domains. However, using constraint propagation, we can only achieve domain consistency, which is an approximation of consistency. Furthermore, the dynamic growth of the constraint network may invalidate some of the earlier configuration decisions. Therefore, in general, backtracking is needed for finding consistent solutions. Backtracking, however, makes the configuration process considerably slow. We eliminate the need for backtracking by imposing some restrictions on the configuration problem (i.e., the model of the product family), and configuring parameters in a certain order. For the latter, we have proposed an algorithm that computes a partial ordering over configurable parameters. We proved that, for configuration problems that conform to the specified restrictions, the ordering approach prevents the need for backtracking, while ensuring consistency. In future, we will study various CPSs to identify what percentage of realistic CPSs conform to the specified restrictions. Furthermore, we will evaluate the improvements that a backtrack-free algorithm can bring about when configuring realistic CPSs.},
  year = {2014},
  journal = {Lyon, France},
  publisher = {CP meets Verification},
  address = {Lyon, France},
}