Research On Model Checking Method-Based Trustworthy Software Verification Technology

With the development of modern society, information infrastructure with the core of communications, storage and computing has gradually penetrated into all aspects of social life. Software system as the core of information infrastructure, is becoming increasingly large and complex. However, software flaws and leaks are difficult to avoid the emergence of software's credibility problem. Trustworthy software is highly reliable nature of the system software. Current research on the credibility of software technology is only at the initial stage, the credibility of the verification of the software more realistic. According to research status on trustworthy software verification technology, the paper based model checking and features of software model checking, to research the trustworthy software verification technology, the main results obtained are:For the existing software model checking approach to the problem of large process efficiency is low, based on reconstruction process technology, introduce a pretreatment method of the pending source code. According to the procedural nature of LTL formula for the composition, gives the reconstruction process after pretreatment program semantics equivalent sufficient conditions for the safety of this method is proved. Specific examples of experimental results illustrate the large-scale program in improving the efficiency of software model checking.Considering in the model checking counter-example guided refinement methods, the abstraction process is calculated by calling the theorem prover, the efficiency is low, a based on SAT solver abstract program construction method is improved. The method uses SAT solver to construct basic blocks and control flow statements in the abstract transition relation in order to generate more precise relationship between abstract process migrations, reducing the model checking process for redundant number of false counter-example to improve the model checking computation efficiency.This paper researchs the problem of counterexamples with loops in model checking predicate abstraction technology. Introduces a new approach to predicate abstraction technique to find a large number of process iteration of the loopholes; presents an algorithm to detect loops in abstract models, describes how the traditional simulation and refinement algorithms can be extended to cope with loops. Results of experimentation show that the method is better than abstraction-refinement method based verification tools BLAST and SLAM.