This project is developing methods to produce software tests, including conformance tests, from specifications. These methods promise significantly more economical means for testing software than are currently available. This will reduce time-to-market for companies producing software products. The project will be successful if the benefit derived from producing tests automatically, rather than current methods, exceeds the cost of producing formal specifications.

Brief Description:

A 28 February 2000 Business Week article states that "security, for everyone, hinges on software quality" and "more real testing - not 'beta testing' in the marketplace - will yield programs that are less vulnerable to attack." To date, most research on automated software testing has focused on structural testing, i.e., testing based on execution paths within the code that implements a specified function. Many practitioners believe the combinatorics of structural testing approaches render them hopeless. In addition, structural testing is not possible with many systems because there is no access to source code. An alternative is to use specification based testing, in which tests are derived from the specification alone.

This project harnesses formal methods to improve the quality of software by automatically generating tests for software from formal specifications. Automated software test generation also greatly reduces the costs of software testing. Deriving tests from specifications is particularly useful for bodies developing software standards, e.g., W3C, OMG, IEEE, and ANSI. The goal of these groups is specification development, while the goal of associated companies is software implementation. This project furthers software quality by companies implementing software to standard specifications by providing a method to automatically generate software tests demonstrating conformance to them. As a result, software products with fewer failures and closer adherence to standards come to the market earlier and at less cost.

Links:

An on-line demonstration showing how an automobile cruise control can be specified and tested.

Staff:

Paul Black, Vadim Okun, Bill Majurski, Jim Lyle

Selected Papers:

There is a more complete list of papers with links to abstracts and whole papers.

Paul Ammann, Paul E. Black, and Wei Ding, Model Checkers in Software Testing, 2002.

Paul E. Black and Scott Ranville, Winnowing Tests: Getting Quality Coverage from a Model Checker without Quantity, 2001.

Paul E. Ammann and Paul E. Black, A Specification-Based Coverage Metric to Evaluate Test Sets, 2000.

Paul E. Black, Vadim Okun, and Yaacov Yesha, Mutation Operators for Specifications, 2000.

Paul Ammann and Paul E. Black, Abstracting Formal Specifications to Generate Software Tests via Model Checking, 1999.

D. Richard Kuhn, Fault Classes and Error Detection in Specification Based Testing, NIST-IR 6140, 1998.

Paul E. Ammann, Paul E. Black, and William J. Majurski, Using Model Checking to Generate Tests from Specifications, 1998.

Updated Thu May 22 11:28:19 2003

The URL of this page is /~black/FTG/autotest.html.