 Automatic
Software Test Generation from Formal Specifications
(http://hissa.nist.gov/~black/FTG/autotest.html)
Dr. Paul E. Black (paul.black@nist.gov)
Overview: This project harnesses formal methods to improve the quality of software by automatically generating tests for software products from formal specifications.
Industry Need Addressed: Up to 50% of the cost of software development is testing. Writing tests is expensive, labor-intensive, and time consuming. As a result, developers often skimp on testing. Compounding this, there is little incentive to go to the expense of formally, i.e., unambiguously and mechanically, specifying software behavior. Formal specifications improve software quality by enabling automated checks for ambiguity, inconsistency, and omission within the specification. Having the technology to automatically generate software tests from high-level formal specifications offsets the cost of developing formal software specifications by significantly reducing the cost of manual software test development.
Deriving tests from specifications is particularly useful for consortia, e.g., W3C, OMG, and formal standards bodies, e.g., IEEE, ANSI, developing standard software specifications. The goal of these groups is specification development. The goal of individual members of these groups is software product development. This project improves the quality of software developed by individual members by providing a method to automatically generate software tests demonstrating conformance to the standard specification. As a result, higher quality software products which use standard specifications come on the market earlier and at less cost.
NIST/ITL Approach: NIST developed a new, innovative method of automatically generating software tests from formal specifications (http://hissa.nist.gov/~black/Papers/icfem98.ps). This method consists of the following steps: generate mutants from the formal specification; analyze the mutant specifications with a model checker to create counterexamples; generate tests from the counterexamples. In cooperation with University of Maryland Baltimore County (UMBC) and George Mason University (GMU), a set of research tools which implement this method has been developed. A demonstration of the method and tools is available at http://hissa.nist.gov/~black/AFTG/. A new metric for the coverage of software tests produced from the method is being developed (http://xsun.sdct.itl.nist.gov/~black/Papers/ijrqse.html). This coverage metric measures how thoroughly the generated set of software tests exercises all aspects of a specification. High-level software specifications usually must be reduced in order to use model checkers. A new reduction was developed, parts of which can be applied mechanically (http://hissa.nist.gov/~black/Papers/finitfocus.ps).
Impact: Under a non-disclosure agreement, the Ford Motor Company submitted logic examples from drivetrain controllers to test the feasibility of the method and tools. If these tests are successful, Ford is interested in seeing the method commercialized with the help of a software development company. In addition, NIST is working with Argus, a secure operating system company, to test the feasibility of the method. Their goal is also to transfer the method to practice. Connie Heitmeyer, an internationally known researcher from the Naval Research Laboratory, is also assessing the method. In addition, conference tracks devoted to automatic test generation from formal specifications are now being held.
|
|
