Abstract Model Generation in Interactive Configuration Tool

Pierre Carbonnelle

In many domains, man-made systems are configured to respond to the demands of the environment. Aspects of the environment and of the configuration are often described by real numbered variables. In that case, constraint theories describing how possible configurations of the system are constrained by the environment typically accept infinitely many models. Sometimes, the user wants to obtain a concrete model of the theory, describing a concrete configuration in a concrete environment. Other times, she prefers an abstract model, representing a class of possible concrete configurations in a class of possible concrete environments, and providing high-level architectural information and applicable ranges for numerical variables. We report on an interactive configuration tool that allows a user to find such abstract models. It uses a proposed refinement of SMT techniques for predicate abstractions. It is generated automatically from constraint theories over infinite domains.