Software inspection apparatus
AssigneeHitachi, Ltd.
InventorMasataka Nishi
Life of this patent
Estimating the term…
Abstract
While the effectiveness of a model inspection method as a means for detecting software defects is known, large-scale software cannot be handled due to great amounts of calculation required for inspection. According to the present invention, after a model inspection problem of software is attributed to be a satisfiability determination problem, the problem is converted to a type that can be solved by a solver used for solving a notification optimization problem having constrained conditions, and the satisfiability is determined in a numerically analytical manner.
Claims6
A software inspection apparatus comprising a processor configured to:
- receive software to be inspected, an input value constraint having an inspection range for an input value to the software, and an inspection condition designating a requirement that the software is to satisfy as input values;
- inspect the software on the basis of the input values;
- and
- output an inspection condition determination result,
- wherein the processor executes the inspection of the software by satisfiability determination using a constrained optimization solver,
- wherein the processor is further configured to:
- convert the software into a constrained partially-ordered graphing SSA format;
- generate a list of constraint formats by merging the input value constraint and the inspection condition;
- generate a list of value range constrained constraint expressions and first and second derivative expressions of the constraint expression from the list of constraint formats;
- and
- convert an output value from the constrained numerical optimization solver into a report on whether or not an overflow in operation occurs and a report on a determination result of the inspection condition.
A software inspection apparatus comprising a processor configured to:
- receive software to be inspected, an input value constraint having an inspection range for an input value to the software, and an inspection condition designating a requirement that the software is to satisfy as input values;
- inspect the software on the basis of the input values;
- and
- output an inspection condition determination result,
- wherein the processor executes the inspection of the software by satisfiability determination using a constrained optimization solver,
- wherein the constrained optimization solver includes:
- a function of outputting an operation position causing overflow in a case where the overflow in operation occurs during a program execution process within a range of the input value constraint;
- and
- a function of outputting a program execution path leading violation of the inspection condition in a case where there is an improper input value that violates the inspection condition, and
- wherein the processor is further configured to:
- convert the software into a constrained partially-ordered graphing SSA format and further generate a list of constraint formats by merging the input value constraint and the inspection condition;
- generate a list of value range constrained constraint expressions and first and second derivative expressions of the constraint expression from the list of constraint formats;
- and
- convert an output value from the constrained numerical optimization solver into a report on whether or not the overflow in operation occurs and a report on a determination result of the inspection condition.
A software inspection apparatus comprising:
- a processor configured to:
- receive software to be inspected, an input value constraint having an inspection range for an input value to the software, and an inspection condition designating a requirement that the software is to satisfy as input values;
- inspect the software on the basis of the input values;
- and
- output an inspection condition determination result,
- wherein the processor executes the inspection of the software by satisfiability determination using a constrained optimization solver,
- wherein the constrained optimization solver includes:
- a function of outputting an operation position causing overflow in a case where the overflow in operation occurs during a program execution process within a range of the input value constraint;
- and
- a function of outputting a program execution path leading violation of the inspection condition in a case where there is an improper input value that violates the inspection condition, and
- wherein the processor is further configured to:
- convert the software into a constrained partially-ordered graphing SSA format;
- and
- generate a list of constraint formats by merging the input value constraint and the inspection condition.
Dependencies are inferred from the claim text.