Skip to main content
SpringerLink
Log in
Book cover

Haifa Verification Conference

HVC 2010: Hardware and Software: Verification and Testing pp 9–22Cite as

An Introduction to Test Specification in FQL

  • Conference paper

Part of the book series: Lecture Notes in Computer Science ((LNPSE,volume 6504))

Abstract

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.

Supported by BMWI grant 20H0804B in the frame of LuFo IV-2 project INTECO and by DFG grant FORTAS – Formal Timing Analysis Suite for Real Time Programs (VE 455/1-1).

This is a preview of subscription content, log in via an institution.

Chapter
USD   29.95
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
eBook
USD   39.99
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
USD   54.99
Price excludes VAT (USA)
  • Compact, lightweight edition
  • Dispatched in 3 to 5 business days
  • Free shipping worldwide - see info

Tax calculation will be finalised at checkout

Purchases are for personal use only

Learn about institutional subscriptions

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. RTCA DO-178B: Software considerations in airborne systems and equipment certification (1992)

    Google Scholar 

  2. Bird, D.L., Munoz, C.U.: Automatic generation of random self-checking test cases. IBM Systems Journal 22(3), 229–245 (1983)

    Article  Google Scholar 

  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. Godefroid, P.: Compositional dynamic test generation. In: Hofmann, M., Felleisen, M. (eds.) POPL, pp. 47–54. ACM, New York (2007)

    Google Scholar 

  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. 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. 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. 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. 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)

    Chapter  Google Scholar 

  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)

    Chapter  Google Scholar 

  11. Beyer, D., Holzer, A., Tautschnig, M., Veith, H.: Directed software verification. Technical Report (2010)

    Google Scholar 

  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. 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. Henzinger, T.A., Jhala, R., Majumdar, R., Sutre, G.: Lazy abstraction. In: POPL, pp. 58–70 (2002)

    Google Scholar 

  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)

    Chapter  Google Scholar 

  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)

    Chapter  Google Scholar 

  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. Beyer, D., Keremoglu, M.E.: Cpachecker: A tool for configurable software verification. CoRR abs/0902.0019 (2009)

    Google Scholar 

  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. 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)

    Chapter  Google Scholar 

  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)

    Chapter  Google Scholar 

  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)

    Chapter  Google Scholar 

  23. Hessel, A., Pettersson, P.: A global algorithm for model-based test suite generation. Electr. Notes Theor. Comput. Sci. 190(2), 47–59 (2007)

    Article  Google Scholar 

  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)

    Chapter  Google Scholar 

  25. Larsen, K.G., Pettersson, P., Yi, W.: Uppaal in a nutshell. STTT 1(1-2), 134–152 (1997)

    Article  MATH  Google Scholar 

  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)

    Chapter  Google Scholar 

  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. 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. 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. 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)

    Chapter  Google Scholar 

  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)

    Chapter  Google Scholar 

  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)

    Chapter  Google Scholar 

  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)

    Chapter  Google Scholar 

  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 

Download references

Author information

Authors and Affiliations

  1. Formal Methods in Systems Engineering, Vienna University of Technology, Austria

    Andreas Holzer, Michael Tautschnig & Helmut Veith

  2. Oxford University Computing Laboratory, UK

    Christian Schallhart

Authors
  1. Andreas Holzer
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Michael Tautschnig
    View author publications

    You can also search for this author in PubMed Google Scholar

  3. Christian Schallhart
    View author publications

    You can also search for this author in PubMed Google Scholar

  4. Helmut Veith
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Editors and Affiliations

  1. IBM Research - Haifa, Haifa University Campus, 31905, Mount Carmel, Haifa, Israel

    Sharon Barner  & Orna Raz  & 

  2. Department of Computer Science, University of California Irvine, Donald Bren Hall, Room 3088, 92697, Irvine, CA, USA

    Ian Harris

  3. Wolfson Building, Parks Road, OX1 3QD, Oxford, UK

    Daniel Kroening

Rights and permissions

Reprints and permissions

Copyright information

© 2011 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

Holzer, A., Tautschnig, M., Schallhart, C., Veith, H. (2011). An Introduction to Test Specification in FQL. In: Barner, S., Harris, I., Kroening, D., Raz, O. (eds) Hardware and Software: Verification and Testing. HVC 2010. Lecture Notes in Computer Science, vol 6504. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-19583-9_5

Download citation

  • DOI: https://doi.org/10.1007/978-3-642-19583-9_5

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-642-19582-2

  • Online ISBN: 978-3-642-19583-9

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation