The Application Of Model Checking In Configuration

Model checking is an automation technique for verifying finite-state concurrent systems to satisfy the specifications. The main idea is to use a structure to represent a parallel system and the specifications which the system needs to satisfy, and then determining whether the system satisfies the given specifications through a variety of search techniques, if met, it will give the proving, otherwise, the counter-example is given. Compared with other Verification technologies, it comes under increasing international attention for having a fully automatic, complete, few requirements to users and generating proofs and so on. Although the restriction of finite state systems to model checking approach is a disadvantage, the states of hardware and network protocols is limited. Under certain restrictive conditions, many infinite-state systems can be verified by the methods of abstraction and induction. So, model checking has become an effective method for the formal verification of system implementation, and has been an increasingly wide range of applications.Based on different knowledge representation and application areas, the current model checking techniques are mainly three kinds, one based-OBDD symbolic model checking proposed by McMillan who had implemented a model checking tool SMV and used the tool to verify the IEEE Future bus + standard (IEEE Standard 896.1-1991) and found a lot of errors that had not been found before. With the SAT solver evolving in the efficiency of its solution, Biere proposed bounded model checking technology, which implements on a limited length of the path. so the discovery of counter-examples becomes more efficient. Some problems that use Based-OBDD symbolic model checking method are inefficient, but applying bounded model checking technology was able to achieve fairly good results. Another model checking technology is "on-the-fly" model checking technology. In the kinds of model checking technology, the system is modeled as an automaton A and negative specification of the system translated into another automaton S. Test whether the intersection of A and S is the empty set. If the intersection is not empty, then generate a counter-example. Different model checking techniques can be applied for different problems.Product configuration problem is a research branch in the artificial intelligence field. With the emergence of mass customization production mode and increasing of personalization requirements of the user, product configuration has been widely applied to various fields from automotive product configuration, computer product configuration to a network resource allocation and so on. Because the model of configuration problem is built by the experts in the field with the modeler, and we think that the experts in the field may sometimes appear to have constructed some mistakes in the product configuration model which may not exist a feasible solution, that is, according to the effective order which the user provides can not be a configurable product. This paper presents the model checking technology to the product configuration problem in the model validation for ensuring the expert in the field to build a correct product configuration model.The original validation of the effectiveness of the configuration issues is most of all the validity of the order data from the user, and it mainly examine the various parameters of generic components in the product model meets the constraints, if it can generate configurable products. However, in the actual product configuration process, is not only the an aspect of product configuration of the user, but also the product design, assembly and manufacturing and so on, these areas also requires us to give an effective way to ensure effectiveness of the product configuration process. In the current literature, we have not found the validation work of consistency and effectiveness of configuration model itself. Therefore, we propose the problem to verify validity of the configuration model itself and use the thinking of the bounded model checking to validate correctness of the configuration model.The main work we have done is that present the knowledge representation for model checking of the configuration issues, and modeling in the configuration problem, we propose the meta-constraint during the general component parameters in a configuration problem is expressed as the general model variable in model checking problem. The generalized constraint of the configuration problem is expressed as the specification of the verification models. The value of variables in the model is Boolean value, so that we can achieve conversion work from the CSP configuration model to model checking problem configuration Model. Because we want to use the SAT solver to verify the correctness of the model, we give the model that need to meet the basic constraints handling strategy. Using our constraint handling strategy, the basic constraints can be converted into the standard form that the SAT solver is able to accept, CNF formulas form. Then, we use the SAT solver to verify a model if meets the constraints given by conditions (specification). If the model satisfies the given constraints, then we say that the model is correct, otherwise, say that the model is incorrect, and experts in the field need to re - Construct the problem model.This paper presents a case study about a computer model of product configuration. We have adopted the model checking process in this simple case. Because of few parameters and constraints, it does not have a complete illustration about our method. We have selected some formulas which contain a number of variables and constraints to test. We can see that the method which we have proposed can better meet the nature of the problem on validation work through the analysis of the results.In addition, we propose such a model method for the configuration problem model to embed into the design and implementation of product configuration model and provide some support for the experts in the field in ensuring the model's correctness.These constraint processing algorithms can be further improved to enhance the efficiency of model checking. The future work that we will do is to apply this method to real projects. Therefore, our work need to further efforts.