A Runtime Error Analysis Method Based on Abstract Interpretation and Model Validation

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, and belongs to the technical field of software testing. Background technique [0002] The continuous expansion of software scale and the continuous increase of complexity not only bring more difficulties to software development, but also bring greater challenges to software testing. Even after rigorous software testing, there is no guarantee that there are no internal errors. Among them, there is a category of errors that may only occur under specific runtime conditions, referred to as "runtime errors". Runtime errors are the most risky of all software errors, and they are also the most difficult to find. They are hidden in the code, and it is difficult for traditional software testing techniques to find these errors. Therefore, some software can run normally on the surface, but may actually cause unexpected system failures. For systems with ...

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