Research And Implementation Of Embedded Program Invariant For Static Testing Based On Abstract Interpretation

The static testing of embedded software does not run the program and less depend the specificity,real-time, embedded of software, so it is the important measures to guarantee the embedded softwarequality and cut back the cost of embedded software. Software attributes as an important test object canreveal potential errors and improve the accuracy of the testing, while little work do about it.Programinvariant is data contract with unchanging nature.It can demonstrate the associated properties of eachvariable of the software, update documentation, algorithms, data structures and other aspects ofinformation of software systems and determine the location of the error. So the static testing ofembedded software about software attributes can use program invariant.The thesis propose a static detection method for program invariant of embedded C source codebased on the theory of abstract interpretation.The program under test through the fundamentalanalysis can obtain the corresponding abstract domain graph, then abstract execute by traversingabstract domain graph to get the executable path of the program, and symbolic execute the executablepath of the program to detect the initial program invariants with function relation and collectionrelation which takes into account the repeatability of the program invariant.This method caneffectively solve the approximate solution of complex problems and reduce system overhead.The thesis propose a test method with program invariant based on the study of the relationship ofpolynomial relation and program invariant.It determines polynomial program and weakestpreconditions by the executable path of the program, and program invariants transfer to polynomialrelations, and abstract analyzes polynomial relation at destination node of polynomial program to findit correct or not, so the verification of correctness of program invariants is completed. It detectsnormative errors through lexical and parsing analysis, then detects the correct program invariant withthe software documentation to find the consistency static errors such as range of values, in addition tothe zero of the documentation, ect. This method eliminates likelihood program invariants andimproves accuracy and efficiency of the detection.Finally, the thesis has used VC++2005to realize static testing system with program invariant andcompleted testing codes of the embedded Linux platform. It verifies the practicality and correctness ofour method by comparing actual results with expected expectations.