An Introduction to Test Specification in FQL

  • Andreas Holzer
  • Michael Tautschnig
  • Christian Schallhart
  • Helmut Veith
Part of the Lecture Notes in Computer Science book series (LNCS, volume 6504)


In a recent series of papers, we introduced a new framework for white-box testing which aims at a separation of concerns between test specifications and test generation engines. We believe that establishing a common language for test criteria will have similar benefits to testing as temporal logic had to model checking and SQL had to databases. The main challenge was to find a specification language which is expressive, simple, and precise. This paper gives an introduction to the test specification language FQL and its tool environment.


Model Check Temporal Logic Test Suite Regular Expression Basic Block 
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.


Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.


  1. 1.
    RTCA DO-178B: Software considerations in airborne systems and equipment certification (1992)Google Scholar
  2. 2.
    Bird, D.L., Munoz, C.U.: Automatic generation of random self-checking test cases. IBM Systems Journal 22(3), 229–245 (1983)CrossRefGoogle Scholar
  3. 3.
    Cadar, C., Dunbar, D., Engler, D.R.: Klee: Unassisted and automatic generation of high-coverage tests for complex systems programs. In: Draves, R., van Renesse, R. (eds.) OSDI, pp. 209–224. USENIX Association (2008)Google Scholar
  4. 4.
    Godefroid, P.: Compositional dynamic test generation. In: Hofmann, M., Felleisen, M. (eds.) POPL, pp. 47–54. ACM, New York (2007)Google Scholar
  5. 5.
    Godefroid, P., Klarlund, N., Sen, K.: Dart: directed automated random testing. In: Sarkar, V., Hall, M.W. (eds.) PLDI, pp. 213–223. ACM, New York (2005)Google Scholar
  6. 6.
    Gulavani, B.S., Henzinger, T.A., Kannan, Y., Nori, A.V., Rajamani, S.K.: Synergy: a new algorithm for property checking. In: Young, M., Devanbu, P.T. (eds.) SIGSOFT FSE, pp. 117–127. ACM, New York (2006)Google Scholar
  7. 7.
    Sen, K., Marinov, D., Agha, G.: Cute: a concolic unit testing engine for c. In: Wermelinger, M., Gall, H. (eds.) ESEC/SIGSOFT FSE, pp. 263–272. ACM, New York (2005)Google Scholar
  8. 8.
    Holzer, A., Schallhart, C., Tautschnig, M., Veith, H.: How did you specify your test suite. In: Pecheur, C., Andrews, J., Nitto, E.D. (eds.) ASE, pp. 407–416. ACM, New York (2010)Google Scholar
  9. 9.
    Holzer, A., Schallhart, C., Tautschnig, M., Veith, H.: Fshell: Systematic test case generation for dynamic analysis and measurement. In: Gupta, A., Malik, S. (eds.) CAV 2008. LNCS, vol. 5123, pp. 209–213. Springer, Heidelberg (2008)CrossRefGoogle Scholar
  10. 10.
    Holzer, A., Schallhart, C., Tautschnig, M., Veith, H.: Query-driven program testing. In: Jones, N.D., Müller-Olm, M. (eds.) VMCAI 2009. LNCS, vol. 5403, pp. 151–166. Springer, Heidelberg (2009)CrossRefGoogle Scholar
  11. 11.
    Beyer, D., Holzer, A., Tautschnig, M., Veith, H.: Directed software verification. Technical Report (2010)Google Scholar
  12. 12.
    Holzer, A., Januzaj, V., Kugele, S., Langer, B., Schallhart, C., Tautschnig, M., Veith, H.: Seamless testing for models and code. Technical Report (2010)Google Scholar
  13. 13.
    Godefroid, P., Kinder, J.: Proving memory safety of floating-point computations by combining static and dynamic program analysis. In: Tonella, P., Orso, A. (eds.) ISSTA, pp. 1–12. ACM, New York (2010)Google Scholar
  14. 14.
    Henzinger, T.A., Jhala, R., Majumdar, R., Sutre, G.: Lazy abstraction. In: POPL, pp. 58–70 (2002)Google Scholar
  15. 15.
    Ball, T.: A theory of predicate-complete test coverage and generation. In: de Boer, F.S., Bonsangue, M.M., Graf, S., de Roever, W.-P. (eds.) FMCO 2004. LNCS, vol. 3657, pp. 1–22. Springer, Heidelberg (2005)CrossRefGoogle Scholar
  16. 16.
    Clarke, E.M., Kroening, D., Lerda, F.: A tool for checking ansi-c programs. In: Jensen, K., Podelski, A. (eds.) TACAS 2004. LNCS, vol. 2988, pp. 168–176. Springer, Heidelberg (2004)CrossRefGoogle Scholar
  17. 17.
    Beyer, D., Henzinger, T.A., Théoduloz, G.: Program analysis with dynamic precision adjustment. In: ASE, pp. 29–38. IEEE, Los Alamitos (2008)Google Scholar
  18. 18.
    Beyer, D., Keremoglu, M.E.: Cpachecker: A tool for configurable software verification. CoRR abs/0902.0019 (2009)Google Scholar
  19. 19.
    Beyer, D., Chlipala, A.J., Henzinger, T.A., Jhala, R., Majumdar, R.: Generating tests from counterexamples. In: ICSE, pp. 326–335. IEEE Computer Society, Los Alamitos (2004)Google Scholar
  20. 20.
    Henzinger, T.A., Jhala, R., Majumdar, R., Sutre, G.: Software verification with blast. In: Ball, T., Rajamani, S.K. (eds.) SPIN 2003. LNCS, vol. 2648, pp. 235–239. Springer, Heidelberg (2003)CrossRefGoogle Scholar
  21. 21.
    Beyer, D., Chlipala, A.J., Henzinger, T.A., Jhala, R., Majumdar, R.: The blast query language for software verification. In: Giacobazzi, R. (ed.) SAS 2004. LNCS, vol. 3148, pp. 2–18. Springer, Heidelberg (2004)CrossRefGoogle Scholar
  22. 22.
    Hessel, A., Larsen, K.G., Mikucionis, M., Nielsen, B., Pettersson, P., Skou, A.: Testing real-time systems using uppaal. In: Hierons, R.M., Bowen, J.P., Harman, M. (eds.) FORTEST. LNCS, vol. 4949, pp. 77–117. Springer, Heidelberg (2008)CrossRefGoogle Scholar
  23. 23.
    Hessel, A., Pettersson, P.: A global algorithm for model-based test suite generation. Electr. Notes Theor. Comput. Sci. 190(2), 47–59 (2007)CrossRefGoogle Scholar
  24. 24.
    Blom, J., Hessel, A., Jonsson, B., Pettersson, P.: Specifying and generating test cases using observer automata. In: Grabowski, J., Nielsen, B. (eds.) FATES 2004. LNCS, vol. 3395, pp. 125–139. Springer, Heidelberg (2005)CrossRefGoogle Scholar
  25. 25.
    Larsen, K.G., Pettersson, P., Yi, W.: Uppaal in a nutshell. STTT 1(1-2), 134–152 (1997)CrossRefzbMATHGoogle Scholar
  26. 26.
    Hong, H.S., Lee, I., Sokolsky, O., Ural, H.: A temporal logic based theory of test coverage and generation. In: Katoen, J.-P., Stevens, P. (eds.) TACAS 2002. LNCS, vol. 2280, pp. 327–341. Springer, Heidelberg (2002)CrossRefGoogle Scholar
  27. 27.
    Tan, L., Sokolsky, O., Lee, I.: Specification-based testing with linear temporal logic. In: Zhang, D., Grégoire, É., DeGroot, D. (eds.) IRI, IEEE Systems, Man, and Cybernetics Society, pp. 493–498 (2004)Google Scholar
  28. 28.
    Visser, W., Pasareanu, C.S., Khurshid, S.: Test input generation with java pathfinder. In: Avrunin, G.S., Rothermel, G. (eds.) ISSTA, pp. 97–107. ACM, New York (2004)Google Scholar
  29. 29.
    Hamon, G., de Moura, L.M., Rushby, J.M.: Generating efficient test sets with a model checker. In: SEFM, pp. 261–270. IEEE Computer Society, Los Alamitos (2004)Google Scholar
  30. 30.
    Geist, D., Farkas, M., Landver, A., Lichtenstein, Y., Ur, S., Wolfsthal, Y.: Coverage-directed test generation using symbolic techniques. In: Srivas, M., Camilleri, A. (eds.) FMCAD 1996. LNCS, vol. 1166, pp. 143–158. Springer, Heidelberg (1996)CrossRefGoogle Scholar
  31. 31.
    Din, G.: Ttcn-3. In: Broy, M., Jonsson, B., Katoen, J.-P., Leucker, M., Pretschner, A. (eds.) Model-Based Testing of Reactive Systems. LNCS, vol. 3472, pp. 465–496. Springer, Heidelberg (2005)CrossRefGoogle Scholar
  32. 32.
    Schieferdecker, I., Dai, Z.R., Grabowski, J., Rennoch, A.: The UML 2.0 testing profile and its relation to TTCN-3. In: Hogrefe, D., Wiles, A. (eds.) TestCom 2003. LNCS, vol. 2644, pp. 79–94. Springer, Heidelberg (2003)CrossRefGoogle Scholar
  33. 33.
    Ben-Asher, Y., Eytani, Y., Farchi, E., Ur, S.: Producing scheduling that causes concurrent programs to fail. In: Ur, S., Farchi, E. (eds.) PADTAD, pp. 37–40. ACM, New York (2006)CrossRefGoogle Scholar
  34. 34.
    Farchi, E., Nir, Y., Ur, S.: Concurrent bug patterns and how to test them. In: IPDPS, p. 286. IEEE Computer Society, Los Alamitos (2003)Google Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 2011

Authors and Affiliations

  • Andreas Holzer
    • 1
  • Michael Tautschnig
    • 1
  • Christian Schallhart
    • 2
  • Helmut Veith
    • 1
  1. 1.Formal Methods in Systems EngineeringVienna University of TechnologyAustria
  2. 2.Oxford University Computing LaboratoryUK

Personalised recommendations