Automated Test Generation with SAL
Grégoire Hamon, Leonardo de Moura, and John Rushby
CSL Technical Note, January 2005
Abstract
We describe sal-atg, a tool for automated test generation
that will be distributed as part of the next release of SAL. Given
a SAL specification augmented with Boolean trap variables
representing test goals, sal-atg generates an efficient set
of tests to drive the trap variables to TRUE; SAL
specifications are typically instrumented with trap variables
representing structural coverage criteria during automatic translation
from a higher-level source notation, such as RSML-e or Stateflow.
We describe extensions to the method of test generation that use
conjunctions of trap variables; we show how these can be used
to provide boundary coverage and to encode test purposes. We
also describe how the output of the tool can be customized to the
requirements of the test harness concerned. We describe experiments
with sal-atg on realistic examples and preparations for
evaluating the quality of tests generated using the experimental
framework of Heimdahl, George and Weber.
gzipped postscript,
or
plain postscript
or
PDF
or
crude ascii (for your Palm Pilot)
Download
sal-atg is part of SAL 3.0, available here
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