Bolong Zeng and Li Tan. Advances in Intelligent Systems and Computing. In Press. Springer. 2014
Buchi automaton is one of the most commonly used formalisms for specifying and reasoning linear temporal properties. It is instrumental for developing formal verification algorithms, i.e., model checkers, for linear temporal logics. Until now Buchi automaton-based specification is mainly used in automated verification in form of linear temporal logic model checking. In this paper, we develop test criteria and techniques that are essential for testing upon specifications in Buchi automata. These criteria measure the semantic relevancy of test cases to a requirement in Buchi automaton. We define “weak” and “strong” variants of the criteria based on coverage on the transitions of the Buchi automaton. These criteria can be used to measure the quality of existing test cases with respect to requirements in Buchi automaton, and to drive test case generation. We develop automated test-case generation algorithms that use an off-the-shelf model checker to generate test cases under these test criteria. In our extended computational study we deploy two methodologies to measure and demonstrate the effectiveness of our approach. First, we measure the cross-coverage of the transition coverage criteria against other existing test criteria. Second, we use a fault-injection technique to measure the sensitivity of our approach. In both cases, our approach shows a better performance compared with existing test criteria and a good sensitivity in detecting errors systematically injected to a system. Furthermore, the proposed criteria uncover not only the deficiency of a test suite with respect to a linear temporal requirement, but also that of the requirement itself. We propose an algorithm to refine the requirement using the feedback from test-case generation.