Research For Abstract Interpretation Based On Configurable Program Analysis

With the rapid development of computer technology,software has become a key factor in determining system safety.Program code as the core of the software,small errors can lead to serious safety incidents.Validation of run-time errors in program is a vital part of ensuring software safety.Commonly used methods in industry such as simulation,emulation,testing can find most of the run-time errors,but there is no guarantee that the software does not have run-time error.Existing formal static analysis methods such as model checking need to exhaustive all state space.There is a state space explosion problem.For theorem proving,it needs a large amount of human intervention and it is difficult to automate.Abstract interpretation makes a balance between analytical precision and analytical efficiency.It is one of the most appropriate analytical methods for the verification of run-time errors.In order to meet the industrial needs,static analysis often needs to adjust according to different needs of the accuracy and efficiency of the analysis process.Configurable Program Analysis is a static analysis framework that adjusts the accuracy and efficiency of the analysis process through configuration parameters,and is suitable for modeling the analysis process of abstract interpretation.This paper presents and extends a framework of static analysis to support abstract interpretation,which is Configurable Program Analysis.The run-time errors are analyzed and validated by using an abstraction analysis based on Configurable Program Analysis to simulate all the possible states of the program in the abstract environment.The main work of the paper is as follows.(1)The formalism of static analysis of Configurable Program Analysis is extended.Firstly,a static analysis formalism which supports abstract interpretation is proposed.Afterwards,explain the termination problem in Configurable Program Analysis.Finally,the Configurable Program Analysis is extended to ensure the termination of the analysis process.(2)Explains how to use the extended Configurable Program Analysis to verify run-time errors.Firstly,the conversion method from source code to program control flow graph is given.After that,configure the corresponding parameters to complete the analysis process of abstract interpretation,in order to obtain the fixpoint of the abstract value.Finally,verify whether the program has run-time errors based on the fixpoint of abstract values.(3)The prototype tool for analyzing and verifying the code runtime error is designed,and the case study of the aircraft Slats and Flaps Control Unit is carried out.Firstly,the design idea of prototype tool based on extended configurable program analysis is given.Then,part of the aircraft Slats and Flaps Control Unit code is analyzed by using the prototype tool.Finally,the analysis results of the prototype tool are given,and some run-time errors of the Slats and Flaps Control Unit are found.