Research Of The Model Checking Method And Technology Guided By Testing Purpose

With the continuous development and progress of computer technology, computer application in the field more widely and deeply. National defense, military and other fields related to national security, and is closely related to the people living in the fields such as bank insurance are closely related to computer technology. It puts forward higher requirements to the reliability of the computer software system. Because the computer development speed and application do not match the actual level, make frequent software failure. On August16,2013, for example, Shanghai Everbright securities trade exception occurs, because a sharp fluctuations of the market in a short period of time, many investors losses due to follow suit comes into play. And the cause of the incident is the everbright securities trading system problems. Therefore, how to ensure the reliability of the software products has become an important problem that must be addressed.Model Checking is an effective method of formal verification. This method can partly solve the software reliability and validity of the problem. Model checking, however, has some shortcomings, that is in the process of verification to complex system state space explosion is produced. To targeted ease state space explosion problem, combined with the software testing technology, in this paper, the model checking method based on the testing purpose guide is studied.This paper focuses on the method and technique which is based on testing purpose, in order to achieve early testing of the code; this paper discusses the model checking method for pseudo code, and to evaluate the detection effect of the method. Specific work contents are as follows:first, analysis the BPEL and LOTOS syntactic and semantic rules design and realize the BPEL to LOTOS automatic conversion tool. BPEL is formal representation of flow diagram, the generation of flow chart is based on the pseudo code of module partition and obtaining the basic path after each module is modeled (this part of the job has completed by another member of the laboratory).Second, analysis and study of μ-calculus description language lexical and grammatical rules, according to the rules to design the implementation algorithm of the lexical analyzer and syntax analyzer, and according to the development of μ-calculus editor is realized. Three, use the μ-calculus editor to describe the basic path under test by μ-calculus language, generate test properties of model checking. And use the CADP which is model checking tool to verify the program under test (that is, LOTOS) whether meet the test attribute.In order to test the effectiveness of the proposed method, use eight queens algorithm, backpacks and philosophers algorithm to do the model checking, verified the BPEL to LOTOS automatic conversion tool and μ-calculus editor’s correctness and the usability, and the feasibility of the model checking was carried out on the pseudo code. And the results show that the method of model checking guided by testing purpose can do the model checking based on pseudo and can relieve the state space explosion problem.