You are granted permission for the non-commercial reproduction, distribution, display, and performance of this technical report in any format. However, this permission is only for a period of 45 (forty-five) days from the most recent time that you verified that this technical report is still available from the Department of Computer Science of the University of Maryland at College Park under terms that include this permission. All other rights are reserved by the author(s).
Specification-based Testing of Reactive Software: Tools and Experiments. Lalita Jategaonkar Jangadeesan. Adam A. Porter. Carlos Puchol. J. Christopher Ramming. Lawrence G. Votta. March 1997.
Testing commercial software is expensive and time consuming. Automated testing methods promise to save a great deal of time and money throughout the software industry. One approach that is well-suited for the reactive systems found in telephone switching systems is specification-based testing. We have built a set of tools to automatically test software applications for biolations of safety properties expressed in temporal logic. out testing system automatically constructs finite state machine oracles corresponding to safety properties, builds test harnesses, and integrates them with the application. The test harness hen generates inputs automatically to test the application. We describe a study examining the feasibility of this approach for testing industrial applications. To conduct this study we formally modeled an Automatic Protection Switching system (APS), which is an application common to many telephony systems. We then asked a number of computer science graduate students to develop several versions of the APS and use our tools to test them. We found that the tools are very effective, save significant amounts of human effort (at the expense of machine resources), and are easy to use. We also discuss improvements that are needed before we can use the tools with professional developer building commercial products. (Also cross-referenced as UMIACS-TR-97-18) University of Maryland Institute for Advanced Computer Studies, Dept. of Computer Science, Univ. of Maryland, Bell Laboratories, Naperville IL, Dept. of Computer Sciences, Univ. of Texas at Austin, AT&T Laboratories,
Specification-based Testing of Reactive Software: A Case Study in. Lalita Jangadeesan. Adam A. Porter. Carlos Puchol. J. Christopher Ramming. Lawrence G. Votta. February 1997.
We describe a case study in which we tried to transfer a specification-based testing system from research to practice. We did the case study in two steps: First we conducted a feasibility study in a laboratory setting to estimate the potential costs and benefits of using the system. Next we conducted a usability study, in an industrial setting, to determine whether it would be effective in practice. The case study illustrates that technology transfer efforts can benefit from a greater focus on practitioners' needs, and that this focus helps identify some of the open problems that limit formal methods technology transfer. We also found that there is often a tension between the scope of the problem to be solved and the specificity of the solution. The greater the scope of the problem, the more general the formal method solution and, thus, the more customization that must be done to use it in a particular environment. We suggest that researchers limit the scope of the problems they try to solve to minimize the risk of technology transfer failure. (Also cross-referenced as UMIACS-TR-97-16) University of Maryland Institute for Advanced Computer Studies, Dept. of Computer Science, Univ. of Maryland,
Last Generated Fri Aug 11 04:01:01 EDT 2000