Specification-based testing with buchi automata: Transition coverage criteria and property refinement

Büchi automaton is instrumental in linear-temporal logic model checking. It has been used in formalizing linear temporal requirements as well as in designing model checking algorithms. In this work we extend Büchi automaton to the domain of specification-based testing. We developed test criteria and techniques essential for testing a system with formal requirements in Büchi automata. At the core of our approach are two Büchi-automaton-based test criteria that select test cases based on their relevancy to a requirement in Büchi automaton. The relevancy is based on the notion of transition coverage on Büchi automaton. We define "weak" and "strong" variants of transition coverage criteria that reflect the non-deterministic nature of a Büchi automaton. 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. To improve test efficiency, we provide model-checking-assisted algorithms that fully automate test vector generations for the transition coverage criteria. In addition, we propose property refinement using the feedback from the test generation algorithm. The benefits of our approach are two-fold: (1) it enables the effective and efficient testing with formal requirements in Büchi automata; and, (2) our approach is capable of not only finding bugs in a system, but also identifying deficiency in its requirements via property refinement.