Skip to main content
SpringerLink
Log in
SpringerLink
Log in

On the Existence of Practical Testers

  • Chapter
  • First Online:
ModelEd, TestEd, TrustEd

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

Abstract

Model-based testing is one of the promising technologies to increase the efficiency and effectiveness of software testing. This paper outlines the evolution of model-based testing based on labelled transition systems, from purely theoretical developments in the eighties to industrially applicable tools now: from canonical testers to practical testers. We present TorXakis as an example of a practical model-based tester, founded in the testing theory for labelled transition systems, and now being introduced in the daily practice of testing.

This work has been supported by NWO-TTW project 13859: Sumbat – Supersizing Model-Based Testing.

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 EPUB and 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

References

  1. Abramsky, S.: Observational equivalence as a testing equivalence. Theoret. Comput. Sci. 53(3), 225–241 (1987)

    Article  MathSciNet  MATH  Google Scholar 

  2. Axini: Testautomatisering. http://www.axini.com

  3. Barrett, C., Conway, C., Deters, M., Hadarean, L., Jovanović, D., King, T., Reynolds, A., Tinelli, C.: CVC4. In: Gopalakrishnan, G., Qadeer, S. (eds.) CAV 2011. LNCS, vol. 6806, pp. 171–177. Springer, Heidelberg (2011). doi:10.1007/978-3-642-22110-1_14

    Chapter  Google Scholar 

  4. Belinfante, A.: JTorX: a tool for on-line model-driven test derivation and execution. In: Esparza, J., Majumdar, R. (eds.) TACAS 2010. LNCS, vol. 6015, pp. 266–270. Springer, Heidelberg (2010). doi:10.1007/978-3-642-12002-2_21

    Chapter  Google Scholar 

  5. Belinfante, A., Feenstra, J., de Vries, R., Tretmans, J., Goga, N., Feijs, L., Mauw, S., Heerink, L.: Formal test automation: a simple experiment. In: Csopaki, G., Dibuz, S., Tarnay, K. (eds.) International Workshop on Testing of Communicating Systems, vol. 12, pp. 179–196. Kluwer Academic Publishers, Dordrecht (1999)

    Chapter  Google Scholar 

  6. van der Bijl, M., Rensink, A., Tretmans, J.: Compositional testing with ioco. In: Petrenko, A., Ulrich, A. (eds.) FATES 2003. LNCS, vol. 2931, pp. 86–100. Springer, Heidelberg (2004). doi:10.1007/978-3-540-24617-6_7

    Chapter  Google Scholar 

  7. Bolognesi, T., Brinksma, E.: Introduction to the ISO specification language LOTOS. Comput. Netw. ISDN Syst. 14, 25–59 (1987)

    Article  Google Scholar 

  8. van den Bos, P., Janssen, R., Moerman, J.: \(n\)-complete test suites for ioco. In: Cavalli, A., Yenigün, H., Yevtushenko, N. (eds.) IFIP International Conference on Testing Software and Systems - ICTSS 2017. LNCS, Springer, Heidelberg (2017). To be published

    Google Scholar 

  9. Brandán Briones, L., Brinksma, E.: A test generation framework for quiescent real-time systems. In: Grabowski, J., Nielsen, B. (eds.) FATES 2004. LNCS, vol. 3395, pp. 64–78. Springer, Heidelberg (2005). doi:10.1007/978-3-540-31848-4_5

    Chapter  Google Scholar 

  10. Briones, L.B., Brinksma, E., Stoelinga, M.: A semantic framework for test coverage. In: Graf, S., Zhang, W. (eds.) ATVA 2006. LNCS, vol. 4218, pp. 399–414. Springer, Heidelberg (2006). doi:10.1007/11901914_30

    Chapter  Google Scholar 

  11. Brinksma, E.: On the existence of canonical testers. Memorandum INF-87-5, University of Twente, Enschede (1987)

    Google Scholar 

  12. Brinksma, E.: A theory for the derivation of tests. In: Aggarwal, S., Sabnani, K. (eds.) Protocol Specification, Testing, and Verification VIII, pp. 63–74. North-Holland (1988)

    Google Scholar 

  13. Brinksma, E.: On the coverage of partial validations. In: Nivat, M., Rattray, C., Rus, T., Scollo, G. (eds.) AMAST1993. Workshops in Computing, pp. 245–252. Springer, London (1994). doi:10.1007/978-1-4471-3227-1_25

    Google Scholar 

  14. Brinksma, E.: Formal methods for conformance testing: theory can be practical. In: Halbwachs, N., Peled, D. (eds.) CAV 1999. LNCS, vol. 1633, pp. 44–46. Springer, Heidelberg (1999). doi:10.1007/3-540-48683-6_6

    Chapter  Google Scholar 

  15. Brinksma, E., Alderden, R., Langerak, R., van de Lagemaat, J., Tretmans, J.: A formal approach to conformance testing. In: de Meer, J., Mackert, L., Effelsberg, W. (eds.) Second International Workshop on Protocol Test Systems, pp. 349–363. North-Holland (1990)

    Google Scholar 

  16. Brinksma, E., Karjoth, G.: A specification of the OSI transport service in LOTOS. In: Protocol Specification, Testing, and Verification IV. North-Holland (1984)

    Google Scholar 

  17. Brinksma, E., Scollo, G., Steenbergen, C.: LOTOS specifications, their implementations and their tests. In: van Bochmann, G., Sarikaya, B. (eds.) Protocol Specification, Testing, and Verification VI, pp. 349–360. North-Holland (1987)

    Google Scholar 

  18. Brinksma, E., Tretmans, J.: Testing transition systems: an annotated bibliography. In: Cassez, F., Jard, C., Rozoy, B., Ryan, M.D. (eds.) MOVEP 2000. LNCS, vol. 2067, pp. 187–195. Springer, Heidelberg (2001). doi:10.1007/3-540-45510-8_9

    Chapter  Google Scholar 

  19. Brinksma, E., Tretmans, J., Verhaard, L.: A framework for test selection. In: Jonsson, B., Parrow, J., Pehrson, B. (eds.) Protocol Specification, Testing, and Verification XI, pp. 233–248. North-Holland (1991)

    Google Scholar 

  20. Chow, T.: Testing software design modeled by finite-state machines. IEEE Trans. Softw. Eng. 4(3), 178–187 (1978)

    Article  MATH  Google Scholar 

  21. Claessen, K., Hughes, J.: QuickCheck: a lightweight tool for random testing of haskell programs. In: International Conference on Functional Programming 2000. ACM Press (2000)

    Google Scholar 

  22. Cok, D.: The SMT-LIBv2 Language and Tools: A Tutorial. GrammaTech Inc., Ithaca (2011)

    Google Scholar 

  23. De Moura, L., Bjørner, N.: Satisfiability modulo theories: introduction and applications. Commun. ACM 54(9), 69–77 (2011)

    Article  Google Scholar 

  24. De Nicola, R.: Extensional equivalences for transition systems. Acta Informatica 24, 211–237 (1987)

    Article  MathSciNet  MATH  Google Scholar 

  25. De Nicola, R., Hennessy, M.: Testing equivalences for processes. Theoret. Comput. Sci. 34, 83–133 (1984)

    Article  MathSciNet  MATH  Google Scholar 

  26. Dijkstra, E.W.: Notes On Structured Programming – EWD249. Technische Hogeschool Eindhoven, Eindhoven, The Netherlands, T.H. Report, 70-WSK-03 (1969)

    Google Scholar 

  27. Eertink, H.: Executing LOTOS specifications: the SMILE tool. In: Bolognesi, T., van de Lagemaat, J., Vissers, C. (eds.) LOTOSphere: Software Development with LOTOS, pp. 221–234. Kluwer Academic Publishers, Dordrecht (1995)

    Chapter  Google Scholar 

  28. van Eijk, P.: Software tools for the specification language LOTOS. Ph.D. thesis, University of Twente, Enschede, The Netherlands (1988)

    Google Scholar 

  29. Engelfriet, J.: Determinacy \(\rightarrow \) (observation equivalence = trace equivalence). Theoret. Comput. Sci. 36(1), 21–25 (1985)

    Article  MathSciNet  MATH  Google Scholar 

  30. Frantzen, L., Tretmans, J., Willemse, T.A.C.: Test generation based on symbolic specifications. In: Grabowski, J., Nielsen, B. (eds.) FATES 2004. LNCS, vol. 3395, pp. 1–15. Springer, Heidelberg (2005). doi:10.1007/978-3-540-31848-4_1

    Chapter  Google Scholar 

  31. Frantzen, L., Tretmans, J., Willemse, T.A.C.: A symbolic framework for model-based testing. In: Havelund, K., Núñez, M., Roşu, G., Wolff, B. (eds.) FATES/RV -2006. LNCS, vol. 4262, pp. 40–54. Springer, Heidelberg (2006). doi:10.1007/11940197_3

    Chapter  Google Scholar 

  32. Gaudel, M.C.: Testing can be formal, too. In: Mosses, P.D., Nielsen, M., Schwartzbach, M.I. (eds.) CAAP 1995. LNCS, vol. 915, pp. 82–96. Springer, Heidelberg (1995). doi:10.1007/3-540-59293-8_188

    Chapter  Google Scholar 

  33. van Glabbeek, R.J.: The linear time - branching time spectrum. In: Baeten, J.C.M., Klop, J.W. (eds.) CONCUR 1990. LNCS, vol. 458, pp. 278–297. Springer, Heidelberg (1990). doi:10.1007/BFb0039066

    Chapter  Google Scholar 

  34. Glabbeek, R.J.: The linear time – branching time spectrum II (the semantics of sequential systems with silent moves). In: Best, E. (ed.) CONCUR 1993. LNCS, vol. 715, pp. 66–81. Springer, Heidelberg (1993). doi:10.1007/3-540-57208-2_6

    Google Scholar 

  35. Groote, J., Mousavi, M.: Modeling and Analysis of Communicating Systems. MIT Press, Cambridge (2014)

    MATH  Google Scholar 

  36. Hartman, A., Nagin, K.: The AGEDIS tools for model based testing. In: International Symposium on Software Testing and Analysis – ISSTA 2004, pp, 129–132. ACM Press, New York (2004)

    Google Scholar 

  37. Haskell: an advanced, purely functional programming language. https://www.haskell.org

  38. Heerink, A.: A bounded queue model relating synchronous and asynchronous communication. Master’s thesis, University of Twente, Enschede, The Netherlands (1993)

    Google Scholar 

  39. Heerink, L.: Ins and outs in refusal testing. Ph.D. thesis, University of Twente, Enschede, The Netherlands (1998)

    Google Scholar 

  40. 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.) Formal Methods and Testing. LNCS, vol. 4949, pp. 77–117. Springer, Heidelberg (2008). doi:10.1007/978-3-540-78917-8_3

    Chapter  Google Scholar 

  41. Hoare, C.: Communicating Sequential Processes. Prentice-Hall, Upper Saddle River (1985)

    MATH  Google Scholar 

  42. ISO: Information Processing Systems, Open Systems Interconnection, LOTOS - A Formal Description Technique Based on the Temporal Ordering of Observational Behaviour. International Standard IS-8807, ISO, Geneve (1989)

    Google Scholar 

  43. Jard, C., Jéron, T.: TGV: theory, principles and algorithms: a tool for the automatic synthesis of conformance test cases for non-deterministic reactive systems. Softw. Tools Technol. Transf. 7(4), 297–315 (2005)

    Article  Google Scholar 

  44. Krichen, M., Tripakis, S.: Black-box conformance testing for real-time systems. In: Graf, S., Mounier, L. (eds.) SPIN 2004. LNCS, vol. 2989, pp. 109–126. Springer, Heidelberg (2004). doi:10.1007/978-3-540-24732-6_8

    Chapter  Google Scholar 

  45. Langerak, R.: A testing theory for LOTOS using deadlock detection. In: Brinksma, E., Scollo, G., Vissers, C.A. (eds.) Protocol Specification, Testing, and Verification IX, pp. 87–98. North-Holland (1990)

    Google Scholar 

  46. Lee, D., Yannakakis, M.: Principles and methods for testing finite state machines - a survey. Proc. IEEE 84(8), 1090–1123 (1996). August

    Article  Google Scholar 

  47. Lynch, N., Tuttle, M.: An introduction to input, output automata. CWI Q. 2(3), 219–246 (1989). Technical report MIT/LCS/TM-373 (TM-351 revised), Massachusetts Institute of Technology, Cambridge, USA (1988)

    MathSciNet  MATH  Google Scholar 

  48. Milner, R.: Communication and Concurrency. Prentice-Hall, Upper Saddle River (1989)

    MATH  Google Scholar 

  49. Mostowski, W., Poll, E., Schmaltz, J., Tretmans, J., Wichers Schreur, R.: Model-based testing of electronic passports. In: Alpuente, M., Cook, B., Joubert, C. (eds.) FMICS 2009. LNCS, vol. 5825, pp. 207–209. Springer, Heidelberg (2009). doi:10.1007/978-3-642-04570-7_19

    Chapter  Google Scholar 

  50. de Moura, L., Bjørner, N.: Z3: an efficient SMT solver. In: Ramakrishnan, C.R., Rehof, J. (eds.) TACAS 2008. LNCS, vol. 4963, pp. 337–340. Springer, Heidelberg (2008). doi:10.1007/978-3-540-78800-3_24

    Chapter  Google Scholar 

  51. Petrenko, A.: Fault model-driven test derivation from finite state models: annotated bibliography. In: Cassez, F., Jard, C., Rozoy, B., Ryan, M.D. (eds.) MOVEP 2000. LNCS, vol. 2067, pp. 196–205. Springer, Heidelberg (2001). doi:10.1007/3-540-45510-8_10

    Chapter  Google Scholar 

  52. Phalippou, M.: Relations d’Implantation et Hypothèses de Test sur des Automates à Entrées et Sorties. Ph.D. thesis, L’Université de Bordeaux I, France (1994)

    Google Scholar 

  53. Phillips, I.: Refusal testing. Theoret. Comput. Sci. 50(2), 241–284 (1987)

    Article  MathSciNet  MATH  Google Scholar 

  54. Selenium - Browser Automation. http://www.seleniumhq.org

  55. Sikuli Script. http://www.sikuli.org

  56. TorXakis. https://github.com/torxakis

  57. Tretmans, J.: HIPPO: a LOTOS simulator. In: van Eijk, P., Vissers, C., Diaz, M. (eds.) The Formal Description Technique LOTOS, pp. 391–396. North-Holland (1989)

    Google Scholar 

  58. Tretmans, J.: Test generation with inputs, outputs, and quiescence. In: Margaria, T., Steffen, B. (eds.) TACAS 1996. LNCS, vol. 1055, pp. 127–146. Springer, Heidelberg (1996). doi:10.1007/3-540-61042-1_42

    Chapter  Google Scholar 

  59. Tretmans, J.: Test generation with inputs, outputs and repetitive quiescence. Softw. Concepts Tools 17(3), 103–120 (1996)

    MATH  Google Scholar 

  60. 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). doi:10.1007/978-3-540-78917-8_1

    Chapter  Google Scholar 

  61. Tretmans, J., Verhaard, L.: A queue model relating synchronous and asynchronous communication. In: Linn, R., Uyar, M. (eds.) Protocol Specification, Testing, and Verification XII, pp. 131–145. No. C-8 in IFIP Transactions, North-Holland (1992)

    Google Scholar 

  62. Vaandrager, F.: On the relationship between process algebra and input/output automata. In: Sixth Annual IEEE Symposium on Logic in Computer Science, pp. 387–398. IEEE Computer Society Press (1991)

    Google Scholar 

  63. Vaandrager, F.: Model learning. Commun. ACM 60(2), 86–95 (2017)

    Article  Google Scholar 

  64. Volpato, M., Tretmans, J.: Towards quality of model-based testing in the ioco framework. In: International Workshop on Joining AcadeMiA and Industry Contributions to Testing Automation - JAMAICA 2013, pp. 41–46. ACM, New York (2013)

    Google Scholar 

Download references

Acknowledgements

I wish to thank Piërre van de Laar for many discussions and for co-developing TorXakis. Piërre van de Laar, Petra van den Bos, and Ramon Janssen are thanked for proofreading this paper.

This contribution was written in honour of Ed Brinksma for the Festschrift on the occasion of his 60th birthday. It gives a survey of the developments in formal approaches to testing, showing the important role of Ed’s work and ideas in shaping this area of scientific as well as applied research: the definition and application of formal methods, process-algebraic modelling, the formalization of testing concepts, and the canonical tester theory as its theoretical foundation. Also my own work on model-based testing is for an important part inspired and influenced by Ed’s work. I wish to thank Ed Brinksma for his inspiration, guidance, and support during many years, both at the University of Twente and at ESI. Ed, thank you, and congratulations with your 60th birthday.

Author information

Authors and Affiliations

  1. TNO - Embedded Systems Innovation, Eindhoven, The Netherlands

    Jan Tretmans

  2. Radboud University, Nijmegen, The Netherlands

    Jan Tretmans

Authors
  1. Jan Tretmans
    View author publications

    You can also search for this author in PubMed Google Scholar

Corresponding author

Correspondence to Jan Tretmans .

Editor information

Editors and Affiliations

  1. RWTH Aachen University, Aachen, Germany

    Joost-Pieter Katoen

  2. University of Twente, Enschede, The Netherlands

    Rom Langerak

  3. University of Twente, Enschede, The Netherlands

    Arend Rensink

Rights and permissions

Reprints and permissions

Copyright information

© 2017 Springer International Publishing AG

About this chapter

Cite this chapter

Tretmans, J. (2017). On the Existence of Practical Testers. In: Katoen, JP., Langerak, R., Rensink, A. (eds) ModelEd, TestEd, TrustEd. Lecture Notes in Computer Science(), vol 10500. Springer, Cham. https://doi.org/10.1007/978-3-319-68270-9_5

Download citation

  • DOI: https://doi.org/10.1007/978-3-319-68270-9_5

  • Published:

  • Publisher Name: Springer, Cham

  • Print ISBN: 978-3-319-68269-3

  • Online ISBN: 978-3-319-68270-9

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation