State coverage metrics for specification-based testing with büchi automata

6Citations
Citations of this article
8Readers
Mendeley users who have this article in their library.
Get full text

Abstract

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. © 2011 Springer-Verlag Berlin Heidelberg.

Cite

CITATION STYLE

APA

Tan, L. (2011). State coverage metrics for specification-based testing with büchi automata. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 6706 LNCS, pp. 171–186). https://doi.org/10.1007/978-3-642-21768-5_13

Register to see more suggestions

Mendeley helps you to discover research relevant for your work.

Already have an account?

Save time finding and organizing research with Mendeley

Sign up for free