Specification transformation and semantic expansion to support automated testing
Mark Blackburn, Paul Ammann · 1998
Software testing will always play a role in the development of software systems. However, testing can account for 40 to 75 percent of the lifetime development and maintenance costs. Although test automation is generally available for test execution, results analysis and coverage analysis, the support for test case generation is rather limited. Formal specifications provide a basis for test case generation. A formal specification provides simple abstract descriptions of the required behaviors describing what the software should do. However, the application of formal specification techniques has not been widespread. A common objection to the use of formal specifications is that the formalisms are difficult to use. Advances in visual model-based development tools provide the basis for developing formal specifications while hiding the formalism. Such tools are increasing in use because they provide tangible benefits by supporting model analysis, simulation, and code generation; however, the underlying models are generally not represented in a form that supports automatic test case generation. This thesis describes rules for transforming model-based specifications into a test specification model that supports automated test case generation and specification-based test coverage analysis. The thesis focuses on model-based specifications that are described using combinations of functional, state transitions and event specifications. The key contribution is the description of transformation rules for specifications composed of combinations of these specification types and associated expansion rules for event specifications. The thesis describes an environment developed to validate the transformation rules. The specific environment is based on a specification translator for the Naval Research Laboratory's Software Cost Reduction (SCR) method and associated tool. The specification translator produces T-VEC specifications from the output of the SCR tool. T-VEC is a tool that produces test vectors and performs specification-based test coverage analysis. Many methods support additional modeling techniques, like hierarchical state transition specifications, in addition to functional, state transition, and event specifications. This thesis provides a foundation for a general framework for conversion and interoperation of models and for reasoning about the relationships among the properties represented by individual models that can be extended to other specification models and techniques.