Patent ID: 8020153
Filing Date: 2011-09-13
Classification: G06F

Abstract:
1. A method of checking source code for a computer program comprising: a path extracting step that extracting an instruction series from the source code along an execution path representing an order for executing the instruction series, the execution path determined by simulating execution of the source code; and a checking information determining step that generating checking information of the source code according to the instruction series extracted in the path extracting step, the checking information corresponding to memory usage of the source code or indicating that the source code has been executed correctly, wherein the checking information determining step includes: a model graph composing step that composing a model graph from the instruction series extracted in the path extracting step; and a model description generating step that generating a model description from the model graph composed in the model graph composing step, wherein both the model graph composing step and the model description generating step are placed before a model checking executing step that performing model checking of the source code according to the model description and specifications expressing a property of checking the source code; and wherein checking of the source code is performed in the model checking executing step according to the model description generated by the model description generating step and preliminarily input specifications.