An introduction to test specification in FQL

Andreas Holzer, Michael Tautschnig, Christian Schallhart, Helmut Veith
[doi] [ISBN] [Google Scholar] [DBLP] [Citeseer]
Read: 23 June 2020

Hardware and Software: Verification and Testing
Springer Berlin Heidelberg
Berlin, Heidelberg
Pages 9-22
2011
Note(s): FQL
Papers: holzer:cav:2008

Proposes a query language FQL for specifying coverage goals that can be used for

  • testcase generation
  • coverage measurement
  • generating code (?)
  • hybrid testing tools based on model checking
  • distributed testcase generation
  • testsuite improvement tools that detect gaps and generate tests to fill them

Path patterns is a good approach for individual tests but not for entire test suites. They need a language for specifying all the path patterns of interest: a meta-regex that specifies sets of regexps using quoted regexps.

The FQL language is specified (see FQL) and there are a number of examples to illustrate the language.

FShell 2 was an interactive frontend and used CBMC as a backend. FShell 3 builds on CPAChecker and can measure the coverage of existing testsuites.

FShell Query Language (FQL)

  • Software verification: Testing vs. model checking [beyer:hvc:2017]
  • FShell: Systematic test case generation for dynamic analysis and measurement [holzer:cav:2008]