Fault Location Research Based On Model Checking

After running the software failure, software fault location is very difficult. The major traditional positioning method is a combination of software testing techniques, use of targeted testing, point out software has a particular defect,and with other ancillary technique find out cause of the malfunction, the existing fault location method have complexity, dependence and low popularization flaws and can not meet the requirements of the software fault diagnosis. Formal methods use mathematical methods, can be better proof of system integrity, accuracy, security. Model checking formal methods in its efficiency, the advantages of automation,and it is now to be used in growing number of areas.Model validation is a important method for verify the temporal logic properties of finite state transition system, since model validation process is completely automated, it is very suitable for the nature of complex system verification requirements, if this technology is used in the fault location, the lack of fault location technology can be filled in some way,and become an important means to improve software reliability.Owing to the needs of current fault location method for software, this paper put forward a software fault location method which based on model validation, and based on this method gives a prototype fault location system framework and some automated in a way. The experiments show that this fault location metod can greatly reduce the scope of the review process of the code and can quickly,efficiently locate software failure, so as to provide a new way for software fault location.The main works include the following:1)Build the formal software model for fault location. Have researched the basic processes of Software model checking, finished the process of making formal software model from source code,designed the data structures and algorithms involved in the modeling process. And analyzed it's performance.2) The reseachof fault location technology based on model verification. With the model establishment, we convert the sematic by combining the tools of model verification, program the suitable code for specific tool, construct the verificatinal fomular, obtain the reversed path with the tools, analyze the information of the reversed path by combining the abstract model, explain the reversed path with the relationship of abstract model and specific system, map the modeling process reversely, and then locate the fault. Meanwhile, build the frame of fault lacation system based on model-verificate-locate process.3) Proceed the fault location experiment using the technology of model verification. using the model verification method in 2) for fault location test, and analyzed the advantages and disadvantages of this method, by proceeding a fault location experiment of one JAVA program which access the shared resource by multi-thread.