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).
Abstract
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.
PDF
BibTeX Entry
TBD
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