Bolong and Li Tan. The 16th IEEE conference on Information Reuse and Integration (IEEE IRI'15). San Francisco, CA. 2015
Büchi 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 requirement in Büchi automaton. At the core of our approach is a metric measuring how well a test suite covers the acceptance condition of a Büchi automaton. Acceptance condition is a key element of Büchi 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. In addition to 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 Büchi 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.