Formal Methods for Test Case Generation

John Rushby, Leonardo De Moura, and Gregoire Hamon

US Patent 7865339, issued 4 January 2011 (filed 12 July 2004).


The invention relates to the use of model checkers to generate efficient test sets for hardware and software systems. The method provides for extending existing tests to reach new coverage targets; searching to some or all of the uncovered targets in parallel; searching in parallel from some or all of the states reached in previous tests; and slicing the model relative to the current set of coverage targets. The invention provides efficient test case generation and test set formation. Deep regions of the state space can be reached within allotted time and memory. The approach has been applied to use of the model checkers of SRI's SAL system and to model-based designs developed in Stateflow. Stateflow models achieving complete state and transition coverage in a single test case are reported.


BibTeX Entry


Having trouble reading our papers?
Return to John Rushby's bibliography page
Return to the Formal Methods Program home page
Return to the Computer Science Laboratory home page