Active property checking

During the last decade, code inspection for standard programming errors has largely been automated with static code analysis. Commercially available static program analysis tools are now routinely used in many software development organizations. These tools are popular because they find many (real) software bugs, thanks to three main ingredients: they are automatic, they are scalable, and they check many properties. In general, a tool that is able to check automatically (with sufficient precision) millions of lines of code against hundreds of coding rules and properties is bound to find on average about one bug (i.e., code error) every thousand lines of code.

As basic code inspection can be achieved using automated code analysis, cost, as part of the software development process, is typically reasonable and manageable. However, a more thorough type of testing, referred to as “software testing”, is a more costly part of the software development process that usually accounts for about 50% of the R&D budget of software development organizations.

Software testing relies on so-called “test cases” or more simply “tests”. To be efficient, tests should be generated in a relevant manner. For example, tests may be generated on the basis of information acquired from analyzing a program. Automating test generation from program analysis can roughly be partitioned into two groups: static versus dynamic test generation. Static test generation consists of analyzing a program statically to attempt to compute input values to drive its executions along specific program paths. In contrast, dynamic test generation consists in executing a program, typically starting with some random inputs, while simultaneously performing a symbolic execution to collect symbolic constraints on inputs obtained from predicates in branch statements along the execution, and then using a constraint solver to infer variants of the previous inputs in order to steer program executions along alternative program paths. Since dynamic test generation extends static test generation with additional runtime information, it can be more powerful.

While aspects of scalability of dynamic test generation have been recently addressed, significant issues exist as to how to dynamically check many properties simultaneously, thoroughly and efficiently, to maximize the chances of finding bugs during an automated testing session.

Traditional runtime checking tools (e.g., Purify, Valgrind and AppVerifier) check a single program execution against a set of properties (such as the absence of buffer overflows, uninitialized variables or memory leaks). Such techniques are referred to herein as traditional passive runtime property checking. As an example, consider the program: int divide (int n, int d) {// n and d are inputs return (n/d); // division-by-zero error if d==0}. The program “divide” takes two integers n and d as inputs and computes their division. If the denominator d is zero, an error occurs. To catch this error, a traditional runtime checker for division-by zero would simply check whether a concrete value of d satisfies (d==0) just before the division is performed for a specific execution run, but it would not provide any insight or guarantee concerning other executions. Further, testing this program with random values for n and d is unlikely to detect the error, as d has only one chance out of 2⁼to be zero if d is a 32-bit integer. Static (and even dynamic) test generation techniques that attempt to cover specific or all feasible paths in a program will also likely miss the error since the program has a single program path which is covered no matter what inputs are used.

While an attempt at checking properties at runtime on a dynamic symbolic execution of a program has been reported, such an approach is likely to return false alarms whenever symbolic execution is imprecise, which is often the case in practice.

Various exemplary methods, devices, systems, etc., are described herein pertain to active property checking. Such techniques can extend runtime checking by checking whether the property is satisfied by all program executions that follow the same program path.

An exemplary method includes providing software for testing; during execution of the software, performing a symbolic execution of the software to produce path constraints; injecting issue constraints into the software where each issue constraint comprises a coded formula; solving the constraints using a constraint solver; based at least in part on the solving, generating input for testing the software; and testing the software using the generated input to check for violations of the injected issue constraints. Such a method can actively check properties of the software. Checking can be performed on a path for a given input using a constraint solver where, if the check fails for the given input, the constraint solver can also generate an alternative input for further testing of the software. Various exemplary methods, devices, systems, etc., are disclosed.

DESCRIPTION OF THE DRAWINGS

Non-limiting and non-exhaustive examples are described with reference to the following figures:

FIG. 1 is a diagram of an exemplary method for active property checking of software;

FIG. 2 is a series of formulas for exemplary side-by-side evaluation of code;

FIG. 3 is a series of formulas for exemplary typing of code;

FIG. 4 is a series of formulas for an exemplary concrete evaluation of code;

FIG. 5 is a series of formulas for an exemplary compliation of code;

FIG. 6 is a series of formulas for an exemplary side-by-side evaluation of code;

FIG. 7 is a listing of a program, the program after cast insertion and corresponding path constraint results;

FIG. 8 is a series of exemplary types for an integer overflow/underflow checker;

Continue reading about Active property checking...
Full patent description for Active property checking

Brief Patent Description - Full Patent Description - Patent Application Claims

Click on the above for other options relating to this Active property checking patent application.
###


How KEYWORD MONITOR works... a FREE service from FreshPatents
1. Sign up (takes 30 seconds). 2. Fill in the keywords to be monitored.
3. Each week you receive an email with patent applications related to your keywords.  
Start now! - Receive info on patent apps like Active property checking or other areas of interest.
###


Previous Patent Application:
Granular measurement of processor performance in executing sections of software code
Next Patent Application:
Method and apparatus for analyzing program execution path
Industry Class:
Data processing: software development, installation, and management

###

Design/code © 2009 FreshContext LLC/Freshpatents.com. Website Terms and Conditions - Also read: About this Page
Patent data source: patents published by the United States Patent and Trademark Office (USPTO)
Information published here is for research/educational purposes only (and in conjunction with our Keyword Monitor) and is not meant to be used in place of the full USPTO patent document/images or a comprehensive patent archive search. Complete official applications are on file at the USPTO and often contain additional data/images (Freshpatents is currently text-only). FreshPatents.com is not affiliated with or endorsed by the USPTO or firms/individuals or products/designs/ideas related to listed patents.

FreshPatents.com Support
Thank you for viewing the Active property checking patent info.
IP-related news and info


Results in 2.30787 seconds


Other interesting Feshpatents.com categories:
Tyco , Unilever , Warner-lambert , 3m paws