发明名称 |
EFFICIENT MODEL CHECKING TECHNIQUE FOR FINDING SOFTWARE DEFECTS |
摘要 |
A method for detecting defects in a computer program. The method steps include obtaining source code and a potential defect definition; identifying, based on the potential defect definition, a set of program objects associated with a potential defect in the source code; extracting an executable program slice having the potential defect from the source code; generating, by a processor, an abstracted model of the program slice by: modeling, using data abstraction, the set of program objects as data-abstracted variables, identifying, within the program slice, a set of control statements including predicates necessary for evaluating the set of control statements, modeling, using predicate abstraction, the predicates as predicate-abstracted Boolean variables, and creating, based on the data-abstracted variables and the predicate-abstracted Boolean variables, a finite state machine (FSM) model of the program slice; and identifying an error state of the FSM indicating an occurrence of the potential defect within the program slice. |
申请公布号 |
US2014229922(A1) |
申请公布日期 |
2014.08.14 |
申请号 |
US201414258902 |
申请日期 |
2014.04.22 |
申请人 |
Oracle International Corporation |
发明人 |
Valdiviezo Basauri Manuel Javier;Cifuentes Cristina N. |
分类号 |
G06F11/36 |
主分类号 |
G06F11/36 |
代理机构 |
|
代理人 |
|
主权项 |
1. A method for detecting defects in a computer program, comprising:
obtaining, by a processor, a plurality of source code and a potential defect definition; identifying, based on the potential defect definition, a plurality of program objects associated with a potential defect in the plurality of source code; extracting an executable program slice having the potential defect from the plurality of source code; generating, by a processor, an abstracted model of the program slice by:
modeling, using data abstraction, the plurality of program objects as a plurality of data-abstracted variables that represent a reduced set of possible states of the plurality of program objects,identifying, within the program slice, a first plurality of control statements comprising a first plurality of predicates necessary for evaluating the first plurality of control statements,modeling, using predicate abstraction, the plurality of predicates as a plurality of predicate-abstracted Boolean variables that represent a reduced set of possible states of the first plurality of control statements, andcreating, based on the plurality of data-abstracted variables and the plurality of predicate-abstracted Boolean variables, a finite state machine (FSM) model of the program slice; and identifying an error state of the FSM indicating an occurrence of the potential defect within the program slice. |
地址 |
Redwood City CA US |