Test case generation algorithm for a model checker

• US 20070250799A1
• Filed: 04/21/2006
• Published: 10/25/2007
• Est. Priority Date: 04/21/2006
• Status: Active Grant

• Current Assignee: Alcatel-Lucent USA, Inc. (Nokia Corporation)
• Original Assignee: Lucent Technologies, Inc. (Nokia Corporation)
• Inventors: Schneider, Axel, Bunin, Grygoriy
• Granted Patent: US 7,523,425 B2
• Time in Patent Office: Days
• US Class Current: 716/106
• CPC Class Codes: G06F 30/3323 using formal methods, e.g. equivalence checking or property checking

Abstract

A method is provided for generating test cases automatically using an abstract system description in combination with a model-checking tool. The abstract system description can be used to design hardware/software systems and the generated test cases can be reused to verify the correctness of the implementation.

Claims

1. A method for test case generation, comprising:

verifying a first property of a system with a model checker;

automatically generating a second property to reach an initial state of a negation of the first property from an initial state of the system;

producing a debug sequence for the second property;

adding at least one internal signal from a last time step of the debug sequence for the second property to an assume part of the negated first property to produce a third property; and

producing a final debug sequence using a concatenation of the second and third properties.

2. The method of claim 1, further comprising:

defining a maximal number of time steps.

3. The method of claim 1, further comprising:

producing a debug sequence for the negated first property.

4. The method of claim 1, further comprising:

producing a debug sequence for the third property.

5. The method of claim 1, further comprising:

mapping a plurality of input signals from the final debug sequence to at least one test procedure.

6. The method of claim 5, further comprising:

adding at least one retrieval procedure to the test procedure.

7. The method of claim 1, further comprising:

providing a test script.

8. A system for test case generation, comprising:

a model checker for providing a plurality of debug sequences; and

a test case generator for using a debug sequence from the model checker for a first property to automatically create a second property to reach an initial state of a negation of the first property from an initial state of a system;

wherein the test case generator adds at least one internal signal from a last time step of the debug sequence for the second property to an assume part of the negated first property to produce a third property;

wherein the model checker produces a final debug sequence using a concatenation of the second and third properties.

9. The system of claim 8, wherein the test case generator receives a maximal number of time steps.

10. The system of claim 8, wherein the model checker verifies the first property and produces a debug sequence for the negated first property.

11. The system of claim 8, wherein the model checker produces a debug sequence for the third property.

12. The system of claim 8, wherein the test case generator maps a plurality of input signals from the final debug sequence to at least one test procedure.

13. The system of claim 12, wherein the test case generator adds at least one retrieval procedure to the test procedure.

14. The system of claim 8, wherein the test case generator provides a test script.

15. A computer readable medium storing instructions for performing a method for test case generation, the method comprising:

verifying a first property of a system with a model checker;

automatically generating a second property to reach an initial state of a negation of the first property from an initial state of the system;

producing a debug sequence for the second property;

adding at least one internal signal from a last time step of the debug sequence for the second property to an assume part of the negated first property to produce a third property; and

producing a final debug sequence using a concatenation of the second and third properties.

16. The computer-readable medium of claim 15, further comprising:

defining a maximal number of time steps.

17. The computer-readable medium of claim 15, further comprising:

producing a debug sequence for the third property.

18. The computer-readable medium of claim 15, further comprising:

mapping a plurality of input signals from the final debug sequence to at least one test procedure.

19. The computer-readable medium of claim 15, further comprising:

adding at least one retrieval procedure to the test procedure.

20. The computer-readable medium of claim 15, further comprising:

providing a test script.