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.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
Similar content being viewed by others
References
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)
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)
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)
Bauer, A., Leucker, M., Schallhart, C.: Runtime verification for LTL and TLTL. ACM Transactions on Software and Methodology (TOSEM) 20 (2011)
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)
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)
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)
Dwyer, M., Avrunin, G., Corbett, J.: Patterns in property specifications for finite-state verification. In: Proc. of ICSE 1999, pp. 411–420 (May 1999)
Fraser, G., Arcuri, A.: Evosuite: Automatic test suite generation for object-oriented software. In: Proc. of ACM SIGSOFT ESEC/FSE, pp. 416–419 (2011)
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)
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)
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)
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)
Kupferman, O., Vardi, M.Y.: Model checking of safety properties. Formal Methods in System Design 19(3), 291–314 (2001)
Meyer, B.: Applying “Design by Contract”. IEEE Computer 25(10), 40 (1992)
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)
Pacheco, C., Ernst, M.D.: Randoop: feedback-directed random testing for Java. In: OOPSLA 2007 Companion, pp. 815–816. ACM, New York (2007)
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)
Pnueli, A.: The temporal logic of programs. In: Proceedings of FOCS 1977, pp. 46–57. IEEE Computer Society, Washington, DC (1977)
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)
Stolz, V., Bodden, E.: Temporal assertions using AspectJ. In: 5th Workshop on Runtime Verification. ENTCS, vol. 144, pp. 109–124. Elsevier (July 2005)
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)
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)
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)
Tong, J., Boulé, M., Zilic, Z.: Defining and providing coverage for assertion-based dynamic verification. Journal of Electronic Testing 26(2), 211–225 (2010)
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)
Veanes, M., Campbell, C., Schulte, W., Tillmann, N.: Online testing with model programs. In: ESEC/SIGSOFT FSE, pp. 273–282. ACM (2005)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights 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)