Formal Specification-Based Testing with Buchi-Automata

CS Colloquium

Date: Tuesday 3/27/2012
Time: 3:30-4:20pm
Location: Room EP 122

The speaker this week is Li Tan, WSU
The talk is titled: Formal Specification-Based Testing with Buchi-Automata

Abstract:
Buchi 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 talk I will present our work that extends specification-based testing to Buchi automata. A key question in specification-based testing is how to measure the quality (relevancy) of test cases with respect to system specification. I will discuss two state coverage metrics for measuring how well a test suite covers a Buchi-automaton-based requirement. Compared with previous work on specification-based testing with temporal logics which are based on the syntactical structure of a temporal logic specification, our new approach emphasizes on testing the semantics relevancy of the specification with respect to the system under test. The new approach improves the effectiveness of specification-based testing with temporal logics, as demonstrated by our experimental results. I will also discuss a model-checking-assisted test generation algorithm that improves the efficiency of test generation.