State Coverage Metrics for Specification-Based Testing with Büchi Automata

Büchi automata have been widely used for specifying linear temporal properties of reactive systems and they are also instrumental for designing efficient model-checking algorithms. In this paper we extend specification-based testing to Büchi automata. A key question in specification-based testing is how to measure the quality (relevancy) of test cases with respect to system specification. We propose two state coverage metrics for measuring how well a test suite covers a Büchi-automaton-based requirement. We also develop test generation algorithms that use counter-example generation capability of an off-the-shelf model checker to generate test cases for the coverage criteria inferred by these metrics. In our experiment we demonstrate the feasibility and performance of the coverage criteria and test generation algorithms for these criteria. In [13] we proposed testing coverage metrics and criteria for properties in Linear Temporal Logic (LTL) and referred to the new approach as property-coverage testing. This research shares the same motivation as in [13] and it extends property-coverage testing to specifications in Büchi automata. Since automaton minimization techniques can be used to reduce the structural diversity of semantically equivalent Büchi automata, we argue that a coverage metric based on Büchi automata is less susceptible to syntactic changes of a property than a LTL-based coverage metric, and hence the proposed coverage metrics measure the relevancy of a test suite to the semantics of a linear temporal property. We also discuss an algorithm for refining a Büchi-automaton-based requirement based on its strong state coverage metric. Our experiment demonstrates the feasibility and performance of our coverage criteria and test generation algorithms.