Nothing Special   »   [go: up one dir, main page]
Skip to main content
Springer Nature Link
Log in

The Integration of Testing and Program Verification

A Position Paper

  • Chapter
  • First Online:
A Journey from Process Algebra via Timed Automata to Model Learning

Part of the book series: Lecture Notes in Computer Science ((LNCS,volume 13560))

Abstract

Formal analysis techniques for software systems are becoming more and more powerful, and have been used on non-trivial examples. We argue that the next step forward is to combine these different techniques in a single framework, which makes it possible to (i) analyse different parts of the system with different techniques, (ii) apply different techniques on a single component, and (iii) seamlessly combine the results of the various analysis. We describe our vision of how this integration can be achieved for the analysis techniques of testing and deductive verification. We end with an overview of research challenges that need to be addressed to achieve this vision.

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

Access this chapter

Log in via an institution

Subscribe and save

Springer+ Basic
$34.99 /Month
  • Get 10 units per month
  • Download Article/Chapter or eBook
  • 1 Unit = 1 Article or 1 Chapter
  • Cancel anytime
Subscribe now

Buy Now

eBook
USD 15.99
Price excludes VAT (USA)
  • Available as EPUB and PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
USD 15.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

Similar content being viewed by others

References

  1. Aarts, F., Kuppens, H., Tretmans, J., Vaandrager, F., Verwer, S.: Learning and testing the bounded retransmission protocol. In: Heinz, J., Higuera, C., Oates, T. (eds.) Proceedings of the Eleventh International Conference on Grammatical Inference, vol. 21. Proceedings of Machine Learning Research. University of Maryland, College Park, pp. 4–18. PMLR (2012). https://proceedings.mlr.press/v21/aarts12a.html

  2. Abbasi, R., Schiffl, J., Darulova, E., Ulbrich, M., Ahrendt, W.: Deductive verification of floating-point Java programs in KeY. In: TACAS 2021. LNCS, vol. 12652, pp. 242–261. Springer, Cham (2021). https://doi.org/10.1007/978-3-030-72013-1_13

    Chapter  MATH  Google Scholar 

  3. Ahrendt, W., Beckert, B., Bubel, R., Hähnle, R., Schmitt, P.H., Ulbrich, M.: Deductive Software Verification the KeY Book, vol. 10001. Springer, Cham (2016). https://doi.org/10.1007/978-3-319-49812-6

    Book  Google Scholar 

  4. Ahrendt, W., Chimento, J.M., Pace, G.J., Schneider, G.: Verifying data- and control-oriented properties combining static and runtime verification: theory and tools. Formal Methods Syst. Des. 51(1), 200–265 (2017). https://doi.org/10.1007/s10703-017-0274-y

    Article  MATH  Google Scholar 

  5. Ammann, P., Outt, J.: Introduction to Software Testing. Cambridge University Press, Cambridge (2016)

    Book  Google Scholar 

  6. Baudin, P., et al.: ACSL: ANSI/ISO C Specification Language, Version 1.14 (2018)

    Google Scholar 

  7. Blom, S., Darabi, S., Huisman, M., Oortwijn, W.: The VerCors tool set: verification of parallel and concurrent software. In: Polikarpova, N., Schneider, S. (eds.) IFM 2017. LNCS, vol. 10510, pp. 102–110. Springer, Cham (2017). https://doi.org/10.1007/978-3-319-66845-1_7

    Chapter  Google Scholar 

  8. van den Bos, P., Jongmans, S.: VeyMont: parallelising verified programs instead of verifying parallel programs. Manuscript

    Google Scholar 

  9. van den Bos, P., Tretmans, J.: Coverage-based testing with symbolic transition systems. In: Beyer, D., Keller, C. (eds.) TAP 2019. LNCS, vol. 11823, pp. 64–82. Springer, Cham (2019). https://doi.org/10.1007/978-3-030-31157-5_5

    Chapter  Google Scholar 

  10. van den Bos, P., Vaandrager, F.W.: State identification for labeled transition systems with inputs and outputs. Sci. Comput. Program. 209, 102678 (2021). https://doi.org/10.1016/j.scico.2021.102678. https://www.sciencedirect.com/science/article/pii/S016764232100071X. ISSN 0167-6423

  11. Broy, M., Jonsson, B., Katoen, J.-P., Leucker, M., Pretschner, A. (eds.): Model-Based Testing of Reactive Systems. LNCS, vol. 3472. Springer, Heidelberg (2005). https://doi.org/10.1007/b137241

    Book  MATH  Google Scholar 

  12. Cok, D.R.: OpenJML: software verification for Java 7 using JML, Open-JDK, and Eclipse. In: Dubois, C., Giannakopoulou, D., Méry, D. (eds.) 1st Workshop on Formal Integrated Development Environment (F-IDE). EPTCS, vol. 149, pp. 79–92 (2014). https://doi.org/10.4204/EPTCS.149.8. https://dx.doi.org/10.4204/EPTCS.149.8

  13. Cok, D.R.: OpenJML: JML for Java 7 by extending OpenJDK. In: Bobaru, M., Havelund, K., Holzmann, G.J., Joshi, R. (eds.) NFM 2011. LNCS, vol. 6617, pp. 472–479. Springer, Heidelberg (2011). https://doi.org/10.1007/978-3-642-20398-5_35

    Chapter  Google Scholar 

  14. Dohrau, J., Summers, A.J., Urban, C., Münger, S., Müller, P.: Permission inference for array programs. In: Chockler, H., Weissenbacher, G. (eds.) CAV 2018. LNCS, vol. 10982, pp. 55–74. Springer, Cham (2018). https://doi.org/10.1007/978-3-319-96142-2_7

    Chapter  Google Scholar 

  15. Fumex, C., Marché, C., Moy, Y.: Automating the verification of floating-point programs. In: Paskevich, A., Wies, T. (eds.) VSTTE 2017. LNCS, vol. 10712, pp. 102–119. Springer, Cham (2017). https://doi.org/10.1007/978-3-319-72308-2_7

    Chapter  Google Scholar 

  16. Galeotti, J., Furia, C., May, E., Fraser, G., Zeller, A.: Inferring loop invariants by mutation, dynamic analysis, and static checking. IEEE Trans. Softw. Eng. 41, 1019–1037 (2015)

    Article  Google Scholar 

  17. Hähnle, R., Huisman, M.: Deductive software verification: from pen-and-paper proofs to industrial tools. In: Steffen, B., Woeginger, G. (eds.) Computing and Software Science. LNCS, vol. 10000, pp. 345–373. Springer, Cham (2019). https://doi.org/10.1007/978-3-319-91908-9_18

    Chapter  MATH  Google Scholar 

  18. Hoare, C.: An axiomatic basis for computer programming. Commun. ACM 12(10), 576–580 (1969). ISSN 0001-0782

    Article  Google Scholar 

  19. Hoder, K., Kovács, L., Voronkov, A.: Invariant generation in vampire. In: Abdulla, P.A., Leino, K.R.M. (eds.) TACAS 2011. LNCS, vol. 6605, pp. 60–64. Springer, Heidelberg (2011). https://doi.org/10.1007/978-3-642-19835-9_7

    Chapter  Google Scholar 

  20. Huertas, T., Quesada-López, C., Martínez, A.: Using model-based testing to reduce test automation technical debt: an industrial experience report. In: Rocha, Á., Ferrás, C., Paredes, M. (eds.) ICITS 2019. AISC, vol. 918, pp. 220–229. Springer, Cham (2019). https://doi.org/10.1007/978-3-030-11890-7_22

    Chapter  Google Scholar 

  21. Jacobs, B., Smans, J., Piessens, F.: Solving the VerifyThis 2012 challenges with VeriFast. Int. J. Softw. Tools Technol. Transfer 17(6), 659–676 (2014). https://doi.org/10.1007/s10009-014-0310-9

    Article  Google Scholar 

  22. Janota, M.: Assertion-based loop invariant generation. In: 1st International Workshop on Invariant Generation (WING) (2007)

    Google Scholar 

  23. Jongmans, S.S., van den Bos, P.: A predicate transformer for choreographies. In: Sergey, I. (ed.) ESOP 2022. LNCS, vol. 13240. Springer, Cham (2022). https://doi.org/10.1007/978-3-030-99336-8_19

    Chapter  Google Scholar 

  24. Karlsson, S., Čaušević, A., Sundmark, D., Larsson, M.: Model-based automated testing of mobile applications: an industrial case study. In: 2021 IEEE International Conference on Software Testing, Verification and Validation Workshops (ICSTW), pp. 130–137 (2021). https://doi.org/10.1109/ICSTW52544.2021.00033

  25. Kosmatov, N., Marché, C., Moy, Y., Signoles, J.: Static versus dynamic verification in Why3, Frama-C and SPARK 2014. In: Margaria, T., Steffen, B. (eds.) ISoLA 2016. LNCS, vol. 9952, pp. 461–478. Springer, Cham (2016). https://doi.org/10.1007/978-3-319-47166-2_32

    Chapter  Google Scholar 

  26. Leavens, G.T., Baker, A.L., Ruby, C.: Preliminary design of JML: a behavioral interface specification language for Java. ACM SIGSOFT Softw. Eng. Notes 31(3), 1–38 (2006)

    Article  Google Scholar 

  27. Leavens, G., et al.: JML reference manual. Department of Computer Science, Iowa State University, February 2007. https://www.jmlspecs.org

  28. Lee, D., Yannakakis, M.: Principles and methods of testing finite state machines-a survey. Proc. IEEE 84(8), 1090–1123 (1996). https://doi.org/10.1109/5.533956

    Article  Google Scholar 

  29. Mattsen, S., Cuoq, P., Schupp, S.: Driving a sound static software analyzer with branch-and-bound. In: 13th IEEE International Working Conference on Source Code Analysis and Manipulation, SCAM 2013, Eindhoven, Netherlands, 22–23 September 2013, pp. 63–68. IEEE Computer Society (2013). https://doi.org/10.1109/SCAM.2013.6648185

  30. Müller, P., Schwerhoff, M., Summers, A.J.: Viper: a verification infrastructure for permission-based reasoning. In: Jobstmann, B., Leino, K.R.M. (eds.) VMCAI 2016. LNCS, vol. 9583, pp. 41–62. Springer, Heidelberg (2016). https://doi.org/10.1007/978-3-662-49122-5_2

    Chapter  MATH  Google Scholar 

  31. Oortwijn, W., Huisman, M., Joosten, S.J.C., van de Pol, J.: Automated verification of parallel nested DFS. In: TACAS 2020. LNCS, vol. 12078, pp. 247–265. Springer, Cham (2020). https://doi.org/10.1007/978-3-030-45190-5_14

    Chapter  Google Scholar 

  32. Pearce, D.J., Utting, M., Groves, L.: An introduction to software verification with Whiley. In: Bowen, J.P., Liu, Z., Zhang, Z. (eds.) SETSS 2018. LNCS, vol. 11430, pp. 1–37. Springer, Cham (2019). https://doi.org/10.1007/978-3-030-17601-3_1

    Chapter  Google Scholar 

  33. Rubbens, R., Lathouwers, S., Huisman, M.: Modular transformation of Java exceptions modulo errors. In: Lluch Lafuente, A., Mavridou, A. (eds.) FMICS 2021. LNCS, vol. 12863, pp. 67–84. Springer, Cham (2021). https://doi.org/10.1007/978-3-030-85248-1_5

    Chapter  Google Scholar 

  34. de Gouw, S., Rot, J., de Boer, F.S., Bubel, R., Hähnle, R.: OpenJDK’s Java.utils.Collection.sort() is broken: the good, the bad and the worst case. In: Kroening, D., Păsăreanu, C.S. (eds.) CAV 2015. LNCS, vol. 9206, pp. 273–289. Springer, Cham (2015). https://doi.org/10.1007/978-3-319-21690-4_16

    Chapter  Google Scholar 

  35. Safari, M., Oortwijn, W., Joosten, S., Huisman, M.: Formal verification of parallel prefix sum. In: Lee, R., Jha, S., Mavridou, A., Giannakopoulou, D. (eds.) NFM 2020. LNCS, vol. 12229, pp. 170–186. Springer, Cham (2020). https://doi.org/10.1007/978-3-030-55754-6_10

    Chapter  Google Scholar 

  36. şakar, Ö., Safari, M., Huisman, M., Wijs, A.: Alpinist: an annotation-aware GPU program optimizer. In: Fisman, D., Rosu, G. (eds.) TACAS 2022. LNCS, vol. 13244, pp. 332–352. Springer, Cham (2022). https://doi.org/10.1007/978-3-030-99527-0_18

    Chapter  Google Scholar 

  37. Sharma, R., Dillig, I., Dillig, T., Aiken, A.: Simplifying loop invariant generation using splitter predicates. In: Gopalakrishnan, G., Qadeer, S. (eds.) CAV 2011. LNCS, vol. 6806, pp. 703–719. Springer, Heidelberg (2011). https://doi.org/10.1007/978-3-642-22110-1_57

    Chapter  Google Scholar 

  38. Tretmans, J.: Model based testing with labelled transition systems. In: Hierons, R.M., Bowen, J.P., Harman, M. (eds.) Formal Methods and Testing. LNCS, vol. 4949, pp. 1–38. Springer, Heidelberg (2008). https://doi.org/10.1007/978-3-540-78917-8_1

    Chapter  Google Scholar 

  39. Tretmans, J.: On the existence of practical testers. In: Katoen, J.-P., Langerak, R., Rensink, A. (eds.) ModelEd, TestEd, TrustEd. LNCS, vol. 10500, pp. 87–106. Springer, Cham (2017). https://doi.org/10.1007/978-3-319-68270-9_5

    Chapter  Google Scholar 

  40. de Vries, R.G., Tretmans, J.: Towards formal test purposes. Formal Approaches Test. Softw. FATES 1, 61–76 (2001)

    Google Scholar 

  41. Zafar, M.N., Afzal, W., Enoiu, E., Stratis, A., Arrieta, A., Sagardui, G.: Model-based testing in practice: an industrial case study using graphwalker. In: 14th Innovations in Software Engineering Conference (Formerly Known as India Software Engineering Conference), ISEC 2021, Bhubaneswar, Odisha, India. Association for Computing Machinery (2021). https://doi.org/10.1145/3452383.3452388. ISBN 9781450390460

  42. Zimmerman, D.M., Nagmoti, R.: JMLUnit: the next generation. In: Beckert, B., Marché, C. (eds.) FoVeOOS 2010. LNCS, vol. 6528, pp. 183–197. Springer, Heidelberg (2011). https://doi.org/10.1007/978-3-642-18070-5_13

    Chapter  Google Scholar 

Download references

Author information

Authors and Affiliations

  1. Formal Methods and Tools, University of Twente, Enschede, The Netherlands

    Petra van den Bos & Marieke Huisman

Authors
  1. Petra van den Bos
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Marieke Huisman
    View author publications

    You can also search for this author in PubMed Google Scholar

Corresponding author

Correspondence to Marieke Huisman .

Editor information

Editors and Affiliations

  1. Radboud University Nijmegen, Nijmegen, The Netherlands

    Nils Jansen

  2. University of Twente, Enschede, The Netherlands

    Mariëlle Stoelinga

  3. University of Twente, Enschede, The Netherlands

    Petra van den Bos

Rights and permissions

Reprints and permissions

Copyright information

© 2022 The Author(s), under exclusive license to Springer Nature Switzerland AG

About this chapter

Check for updates. Verify currency and authenticity via CrossMark

Cite this chapter

van den Bos, P., Huisman, M. (2022). The Integration of Testing and Program Verification. In: Jansen, N., Stoelinga, M., van den Bos, P. (eds) A Journey from Process Algebra via Timed Automata to Model Learning . Lecture Notes in Computer Science, vol 13560. Springer, Cham. https://doi.org/10.1007/978-3-031-15629-8_28

Download citation

  • DOI: https://doi.org/10.1007/978-3-031-15629-8_28

  • Published:

  • Publisher Name: Springer, Cham

  • Print ISBN: 978-3-031-15628-1

  • Online ISBN: 978-3-031-15629-8

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation