Skip to main content
SpringerLink
Log in

Online Testing of LTL Properties for Java Code

  • Conference paper
Hardware and Software: Verification and Testing (HVC 2013)

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

Included in the following conference series:

Abstract

LTL specifications are commonly used in runtime verification to describe the requirements about the system behavior. Efficient techniques derive, from LTL specifications, monitors that can check if system executions respect these properties. In this paper we present an online testing approach which is based on LTL properties of Java programs. We present an algorithm able to derive and execute test cases from monitors for LTL specifications. Our technique actively tests a Java class, avoids false failures, and it is able to check the correctness of the outputs also in the presence of nondeterminism. We devise several coverage criteria and strategies for visiting the monitors, providing different qualities in terms of test size, testing time, and fault detection capability.

This work is partially supported by GenData 2020, a MIUR PRIN 2010-11 project.

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

Access this chapter

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

Institutional subscriptions

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. Alur, R., Courcoubetis, C., Yannakakis, M.: Distinguishing tests for nondeterministic and probabilistic machines. In: Proc. of the 27th Annual ACM Symposium on Theory of Computing, STOC 1995, pp. 363–372. ACM, New York (1995)

    Google Scholar 

  2. Arcaini, P., Gargantini, A., Riccobene, E.: CoMA: Conformance Monitoring of Java Programs by Abstract State Machines. In: Khurshid, S., Sen, K. (eds.) RV 2011. LNCS, vol. 7186, pp. 223–238. Springer, Heidelberg (2012)

    Chapter  Google Scholar 

  3. Artho, C., Barringer, H., Goldberg, A., Havelund, K., Khurshid, S., Lowry, M., Pasareanu, C., Roşu, G., Sen, K., Visser, W., Washington, R.: Combining test case generation and runtime verification. Theoretical Computer Science 336(2-3), 209–234 (2005)

    Article  MathSciNet  MATH  Google Scholar 

  4. Bauer, A., Leucker, M., Schallhart, C.: Runtime verification for LTL and TLTL. ACM Transactions on Software and Methodology (TOSEM) 20 (2011)

    Google Scholar 

  5. Chen, F., Roşu, G.: Java-MOP: A monitoring oriented programming environment for Java. In: Halbwachs, N., Zuck, L.D. (eds.) TACAS 2005. LNCS, vol. 3440, pp. 546–550. Springer, Heidelberg (2005)

    Chapter  Google Scholar 

  6. d’Amorim, M., Ros̨u, G.: Efficient monitoring of ω-languages. In: Etessami, K., Rajamani, S.K. (eds.) CAV 2005. LNCS, vol. 3576, pp. 364–378. Springer, Heidelberg (2005)

    Chapter  Google Scholar 

  7. Duret-Lutz, A., Poitrenaud, D.: SPOT: An extensible model checking library using transition-based generalized Büchi automata. In: MASCOTS 2004, pp. 76–83 (October 2004)

    Google Scholar 

  8. Dwyer, M., Avrunin, G., Corbett, J.: Patterns in property specifications for finite-state verification. In: Proc. of ICSE 1999, pp. 411–420 (May 1999)

    Google Scholar 

  9. Fraser, G., Arcuri, A.: Evosuite: Automatic test suite generation for object-oriented software. In: Proc. of ACM SIGSOFT ESEC/FSE, pp. 416–419 (2011)

    Google Scholar 

  10. Fraser, G., Wotawa, F.: Nondeterministic testing with linear model-checker counterexamples. In: Proc. of the 7th International Conference on Quality Software, QSIC 2007, pp. 107–116. IEEE Computer Society, Washington, DC (2007)

    Google Scholar 

  11. Gallegos, A., Ochoa, O., Gates, A., Roach, S., Salamah, S., Vela, C.: A property specification tool for generating formal specifications: Prospec 2.0. In: Proceedings of SEKE, Los Angeles, CA (2008)

    Google Scholar 

  12. Gross, F., Fraser, G., Zeller, A.: Search-based system testing: high coverage, no false alarms. In: Proceedings of the 2012 International Symposium on Software Testing and Analysis, ISSTA 2012, pp. 67–77. ACM, New York (2012)

    Chapter  Google Scholar 

  13. Kähkönen, K., Lampinen, J., Heljanko, K., Niemelä, I.: The LIME interface specification language and runtime monitoring tool. In: Bensalem, S., Peled, D.A. (eds.) RV 2009. LNCS, vol. 5779, pp. 93–100. Springer, Heidelberg (2009)

    Chapter  Google Scholar 

  14. Kupferman, O., Vardi, M.Y.: Model checking of safety properties. Formal Methods in System Design 19(3), 291–314 (2001)

    Article  MathSciNet  MATH  Google Scholar 

  15. Meyer, B.: Applying “Design by Contract”. IEEE Computer 25(10), 40 (1992)

    Article  Google Scholar 

  16. Nobakht, B., Bonsangue, M.M., de Boer, F.S., de Gouw, S.: Monitoring method call sequences using annotations. In: Barbosa, L.S., Lumpe, M. (eds.) FACS 2010. LNCS, vol. 6921, pp. 53–70. Springer, Heidelberg (2012)

    Chapter  Google Scholar 

  17. Pacheco, C., Ernst, M.D.: Randoop: feedback-directed random testing for Java. In: OOPSLA 2007 Companion, pp. 815–816. ACM, New York (2007)

    Google Scholar 

  18. Pecheur, C., Raimondi, F., Brat, G.: A formal analysis of requirements-based testing. In: Proc. of ISSTA 2009, pp. 47–56. ACM, New York (2009)

    Google Scholar 

  19. Pnueli, A.: The temporal logic of programs. In: Proceedings of FOCS 1977, pp. 46–57. IEEE Computer Society, Washington, DC (1977)

    Google Scholar 

  20. Steven, J., Chandra, P., Fleck, B., Podgurski, A.: jRapture: A capture/replay tool for observation-based testing. In: Proceedings of ISSTA 2000, pp. 158–167. ACM, New York (2000)

    Google Scholar 

  21. Stolz, V., Bodden, E.: Temporal assertions using AspectJ. In: 5th Workshop on Runtime Verification. ENTCS, vol. 144, pp. 109–124. Elsevier (July 2005)

    Google Scholar 

  22. Tabakov, D., Vardi, M.Y.: Optimized temporal monitors for systemC. In: Barringer, H., et al. (eds.) RV 2010. LNCS, vol. 6418, pp. 436–451. Springer, Heidelberg (2010)

    Chapter  Google Scholar 

  23. Tan, L.: State coverage metrics for specification-based testing with Büchi automata. In: Gogolla, M., Wolff, B. (eds.) TAP 2011. LNCS, vol. 6706, pp. 171–186. Springer, Heidelberg (2011)

    Chapter  Google Scholar 

  24. Tan, L., Sokolsky, O., Lee, I.: Specification-based testing with linear temporal logic. In: Proc. of Information Reuse and Integration, pp. 493–498. IEEE (2004)

    Google Scholar 

  25. Tong, J., Boulé, M., Zilic, Z.: Defining and providing coverage for assertion-based dynamic verification. Journal of Electronic Testing 26(2), 211–225 (2010)

    Article  Google Scholar 

  26. Tretmans, J.: Model based testing with labelled transition systems. In: Hierons, R.M., Bowen, J.P., Harman, M. (eds.) FORTEST. LNCS, vol. 4949, pp. 1–38. Springer, Heidelberg (2008)

    Chapter  Google Scholar 

  27. Veanes, M., Campbell, C., Schulte, W., Tillmann, N.: Online testing with model programs. In: ESEC/SIGSOFT FSE, pp. 273–282. ACM (2005)

    Google Scholar 

Download references

Author information

Authors and Affiliations

  1. Dipartimento di Informatica, Università degli Studi di Milano, Italy

    Paolo Arcaini & Elvinia Riccobene

  2. Dipartimento di Ingegneria, Università di Bergamo, Italy

    Angelo Gargantini

Authors
  1. Paolo Arcaini
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Angelo Gargantini
    View author publications

    You can also search for this author in PubMed Google Scholar

  3. Elvinia Riccobene
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Editors and Affiliations

  1. Department of Electrical Engineering and Computer Science, CSE #4645 - ACAL Lab, University of Michigan, 2260 Hayward Avenue, 48109-2121, Ann Arbor, MI, USA

    Valeria Bertacco

  2. Inventors for the Digital World, inria, Bat C, Burean C213, Campus Universitaire de Beaulieu, 35042, Rennes Cedex, France

    Axel Legay

Rights and permissions

Reprints and permissions

Copyright information

© 2013 Springer International Publishing Switzerland

About this paper

Cite this paper

Arcaini, P., Gargantini, A., Riccobene, E. (2013). Online Testing of LTL Properties for Java Code. In: Bertacco, V., Legay, A. (eds) Hardware and Software: Verification and Testing. HVC 2013. Lecture Notes in Computer Science, vol 8244. Springer, Cham. https://doi.org/10.1007/978-3-319-03077-7_7

Download citation

  • DOI: https://doi.org/10.1007/978-3-319-03077-7_7

  • Publisher Name: Springer, Cham

  • Print ISBN: 978-3-319-03076-0

  • Online ISBN: 978-3-319-03077-7

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation