Proceedings of 2014 IEEE Information Reuse and Integration (IEEE IRI'14). Li Tan and Bolong Zeng. IEEE Press. San Francisco, CA. August, 2014.
Buchi automaton is instrumental in linear-temporal logic model checking. It has been used in formalizing linear temporal requirements of a system and designing model checking algorithms. In this work we extend the benefits of B¨uchi automaton to the area of specification-based testing. At the core of our approach are two B¨uchi-automaton-based test criteria that select test cases based on their relevancy to a formal specification in B¨uchi automaton. The relevancy is established using the notion of transition coverage on Buchi-automaton. We define “weak” and “strong” variants of transition coverage criteria that reflect the non-deterministic nature of a Buchi automaton. These two variants address the needs of different test applications. This work extends our previous work on state coverage criteria for B¨uchi automaton. The new transitioncoverage criteria provide better coverage than their statecoverage counterparts both in theory and in our experiment. Our experiment demonstrates the effectiveness of the proposed transition-coverage criteria by measuring cross-coverage of these transition-coverage criteria versus other existing test criteria. We provide model-checking-assisted algorithms for generating tests for the proposed transition-coverage criteria. In addition, we show that the feedback from test generation can be used to refine the specification, and provide an algorithm to automate the refinement process. This requirement refinement technique will help close the loop between requirement engineering and testing by establishing a formal feedback link between two.