Practical Techniques for Automated Specification-Based Testing

Formal methods hold the most potential to raise the level of rigor in the development of software. Unfortunately, they have had only limited penetration into software development practice, due in part to their cost. In this paper, we summarize prior work, performed in collaboration with other researchers, on a specification-based testing approach called boun ed exhaustive testing(BET). We then describe two aspects of current research for reducing the cost of applying this approach in practice: providing developers with easy-to-use test input generation tools, and providing cost-effective alternatives to oracle implementations. By providing software developers with more user-friendly tools and techniques for specification-based testing, we seek to make the BET approach easier to apply in practice, and to encourage the use of formal methods in software development more generally.