Test reactive systems with Buchi automata: acceptance condition coverage criteria and performance evaluation

Buchi automata have been used to specify and reason linear temporal requirements of reactive systems. A reactive system interacts with its environment constantly, and its executions may be modeled as infinite words. A key question in testing a reactive system is how to make testing relevant to the system's requirement, that is, to focus testing on the required behaviors in terms of infinite words. We propose a specification-based testing technique that tests a reactive system with respect to its requirements in Buchi automaton. At the core of our approach are metrics measuring how well a test suite covers the acceptance condition of a Buchi automaton. Acceptance condition is a key element of Buchi automaton defining infinite words. We propose weak and strong variants of coverage metrics and their related test criteria for applications requiring tests of different strengths. We propose a model-checking-assisted algorithm to automate test case generation for proposed criteria. Besides debugging a system, our proposed approach may be used for revealing problems with system requirements. We propose an algorithm for refining a requirement encoded in Buchi automaton. Finally, we evaluate the performance of the proposed test criteria using cross-coverage comparison. The result indicates that our approach improves the effectiveness of testing with more efficient test cases targeted for system requirements.