Verification of computer software
First Claim
1. A method of verifying a computer source code having a series of program statements, including control statements which provide for branching to alternative statements of the code, said method comprising:
- instrumenting the source code to generate when the code is executed an indication for each block of code that the statements of that block have been executed, a block of code being the program statements between control statements;
selecting test cases, with each test case comprising input values for variables in the source code, said test cases being selected such that each block of code is executed;
generating a test driver routine to implement the test cases;
compiling and linking the test driver routine with the instrumented source code;
executing the compiled/linked code to implement the test cases, andgenerating an output with said indication of each block of code which has been executed by the test cases.
1 Assignment
0 Petitions
Accused Products
Abstract
A computer program is verified, unit by unit, by automatically instrumentating the code and generating a test driver program which executes all branches of an instrumented code unit. The code is instrumented by operating processors to standardize the code format and to insert executable tracer statements into each block of reformatted code between control statements. A pseudocode having only control statements and tables identifying valid linkages between blocks of code are generated by another processor for use by a verifier in selecting values of input variables and expected outputs for test cases which execute each block of code in the selected unit. Another processor generates the test driver program from the test cases and a software test specification identifying the test cases and expected results. The test driver program and instrumented code unit are compiled and linked to repeatively execute the instrumented code unit to implement all the test cases. Results of the test cases are printed out indicating the sequence of block linkages generated by each test case, the expected output values and the actual output values.
-
Citations
24 Claims
-
1. A method of verifying a computer source code having a series of program statements, including control statements which provide for branching to alternative statements of the code, said method comprising:
-
instrumenting the source code to generate when the code is executed an indication for each block of code that the statements of that block have been executed, a block of code being the program statements between control statements; selecting test cases, with each test case comprising input values for variables in the source code, said test cases being selected such that each block of code is executed; generating a test driver routine to implement the test cases; compiling and linking the test driver routine with the instrumented source code; executing the compiled/linked code to implement the test cases, and generating an output with said indication of each block of code which has been executed by the test cases. - View Dependent Claims (2, 3, 4, 5, 6, 7, 8, 9, 10, 11)
-
-
12. A method of verifying a computer program source code having a series of program statements including control statements by which the program can branch to alternative statements, said method comprising:
-
size the format of operating a processor to standard the source code to a set of prescribed formatting standards to generate a reformatted source code; selecting a target unit of the reformatted source code for verification; instrumenting said target unit of code by operating a processor to divide said target unit into blocks of code, a block of code being the non-control statements between control statements, and to insert into said blocks of code executable instructions to write to an output file an identifier for each block of code when it is executed; selecting test cases for said target unit of code with each test case comprising input values for variables in the target unit and expected output values, said test cases being selected such that each block of code in the test unit is executed; operating a processor to generate a test driver routine to implement said test cases; operating a processor to compile and link the test driver routine with the instrumented target unit of code; executing the compiled/linked test driver routine and instrumented target unit of code; and generating an output presenting actual output values and expected output values for each test case, and a sequential listing from said output file of the block identifiers of the blocks of said target unit code in the sequence in which they were executed. - View Dependent Claims (13, 14, 15, 16, 17, 18, 19, 20)
-
-
21. A method of verifying software for microprocessors in control and protection systems for a nuclear power plant wherein said software comprises source code having a series of program statements, including . control statements by which the program can branch to alternative statements, said method comprising:
-
loading said source code into a general purpose digital computer; operating said digital computer to standardize the format of the source code in accordance with a set of prescribed formatting standards to generate a reformatted source code; selecting a target unit of the reformatted of the source code for verification; operating said digital computer to instrument said target unit of code by dividing said target unit into blocks of code, a block of code being the non-control statements between control statements, and to insert into the beginning of each block of code an instruction to write to an output file a unique identifier for that block of code when it is executed, and to insert at the end of each block of code an instruction to write to the output file the unique identifier of the block of code to which the target unit reverts; selecting test cases for said target unit of code with each test case comprising input values for variables in the target unit and expected output values, said test cases being selected such that each block of code in the test unit is executed; operating said digital computer to generate a test driver routine to implement said test cases; operating the digital computer to compile and link the test driver routine with the instrumented target unit of code;
operating the digital computer to execute the compiled/linked test driver routine and instrumented target unit of code; andoperating the digital computer to generate an output presenting actual output values and expected output values for each test case, and a sequential listing from said output file of the block identifiers of the blocks of said target unit code in the sequence in which they were executed. - View Dependent Claims (22)
-
-
23. A system for verifying computer program source code having a series of statements, including control statements by which the program can branch to alternative statements, said system comprising:
-
means for instrumenting the source code by dividing the code into blocks of code, a block of code being the non-control statements between control statements, and to insert into said blocks of code executable instructions to write to an output file an identifier for each block of code when it is executed; means for generating a variable file containing the input value of selected input variables of the source code and expected output values for output variables of the source code for selected test cases, said test cases being selected such that each block of code is executed; means for generating a test driver routine utilizing the values in the variable file to implement the test cases; means for compiling and linking the test driver routine with the instrumented source code; means for executing the compiled/linked test driver routine and the instrumented source code to generate actual output values and to write to the output file an identifier for each block of each executed; and means for generating an output presenting said actual output values generated by said executing means and the expected output values contained in said variable file for each test case, and a sequential listing from said output file of the block identifiers of the blocks of said source code in the sequence in which they were executed. - View Dependent Claims (24)
-
Specification