Runtime error analytical method based on abstract interpretation and model verification

Abstract

The invention discloses a runtime error analytical method based on abstract interpretation and model verification. The method includes the following steps that on the basis of the abstract interpretation theory, the program numerical variable value range is analyzed by the adoption of a forward iteration method, the variable value range information is obtained when program points are stable, and the iterative computations of loop nodes are achieved by the way that loop unrolling and delay widening are combined; the variable value range information at the relevant program points needing to be detected is converted to be in an assertion or hypothesis mode to be plugged into a program according to a runtime error type to be analyzed; the assertion or hypothesis programs are converted into a Boolean formula, wherein the Boolean formula comprises limiting conditions and attributes; the correctness of the attributes in the Boolean formula is judged through an SAT verifier, if correct, it shows that relevant runtime errors do not exist, if not correct, it shows that the relevant runtime errors exist, and relevant counter example paths are output. By means of the method, an equilibrium point is acquired between runtime error analysis precision and efficiency.

Description

technical field [0001] The invention relates to a runtime error analysis method based on abstract interpretation and model verification, belonging to the technical field of software testing. Background technique [0002] The continuous expansion of software scale and the continuous improvement of complexity not only bring more difficulties to software development, but also bring greater challenges to software testing. Even rigorous software testing cannot guarantee that it is bug-free. Among them, there is a type of error that may occur only under specific runtime conditions, referred to as "runtime errors". Runtime errors are the most risky of all software errors, and are also the most difficult to find. They are hidden in the code, and traditional software testing techniques are difficult to find these errors. As a result, some software may appear to be working properly, but in fact may cause unexpected system failures. For systems with very high safety requirements suc...

AI Technical Summary

Problems solved by technology

[0004] However, both abstract interpretation and model verification have their own shortcomings: 1. In the process of program value variable analysis based on abstract interpretation, for the value range analysis in the loop statement, in order to ensure the convergence of the loop iteration, the widening operator is generally used to Realized, but the widening operation brings a huge loss of calculation accuracy

2. For large-scale programs, the number of attributes that need to be verified in model verification is huge, the verification efficiency is low, and for infinite systems, the state space will explode

Images