Test case generation algorithm for a model checker
View Patent ↗A method for testing hardware and software system design. An abstract system description is used to design hardware/software systems and generated test cases are reused to verify the correctness of the implementation.
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 by concatenating 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; and
wherein the model checker produces a final debug sequence by concatenating 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 storage device having stored thereon instructions that when executed perform 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 by concatenating the second and third properties.
16. The computer storage device of claim 15 , wherein the method further comprises:
defining a maximal number of time steps.
17. The computer storage device of claim 15 , wherein the method further comprises:
producing a debug sequence for the third property.
18. The computer storage device of claim 15 , wherein the method further comprises:
mapping a plurality of input signals from the final debug sequence to at least one test procedure.
19. The computer storage device of claim 15 , wherein the method further comprises:
adding at least one retrieval procedure to the test procedure.
20. The computer storage device of claim 15 , wherein the method further comprises:
providing a test script.