Automated Test Generation with SAL

Grégoire Hamon, Leonardo de Moura, and John Rushby

CSL Technical Note, January 2005


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)


sal-atg is part of SAL 3.0, available here

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