SpringerLink
Log in

Symbolic Path-Guided Test Cases for Models with Data and Time

  • Conference paper
  • First Online:
Formal Aspects of Component Software (FACS 2023)

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

Included in the following conference series:

  • 91 Accesses

Abstract

This paper focuses on generating test cases from timed symbolic transition systems. At the heart of the generation process are symbolic execution techniques on data and time. Test cases look like finite symbolic trees with verdicts on their leaves and are based on a user-specified finite symbolic path playing the role of a test purpose. Generated test cases handle data involved in time constraints and uninitialized parameters, leveraging the advantages of symbolic execution techniques.

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
EUR 32.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

Chapter
EUR 29.95
Price includes VAT (Germany)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
eBook
EUR 48.14
Price includes VAT (Germany)
  • Available as EPUB and PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
EUR 62.05
Price includes VAT (Germany)
  • Compact, lightweight edition
  • Dispatched in 3 to 5 business days
  • Free ship** worldwide - see info

Tax calculation will be finalised at checkout

Purchases are for personal use only

Institutional subscriptions

Similar content being viewed by others

Notes

  1. 1.

    with the convention that \(\bigwedge \) quantified over empty conditions is the formula True.

  2. 2.

    For i and j in \(\mathbb {N}\) verifying \(i < j\), [i, j) contains the integers from i to \(j-1\) included.

References

  1. Aichernig, B.K., Tappler, M.: Symbolic input-output conformance checking for model-based mutation testing. In: USE@FM 2015, Elsevier (2015). https://doi.org/10.1016/j.entcs.2016.01.002

  2. Alur, R., Dill, D.L.: A theory of timed automata. Theor. Comput. Sci. (1994). https://doi.org/10.1016/0304-3975(94)90010-8

    Article  MathSciNet  Google Scholar 

  3. Andrade, W.L., Machado, P.D.L., Jéron, T., Marchand, H.: Abstracting time and data for conformance testing of real-time systems. In: ICST Workshops (2011). https://doi.org/10.1109/ICSTW.2011.82

  4. Bannour, B., Escobedo, J.P., Gaston, C., Le Gall, P.: Off-line test case generation for timed symbolic model-based conformance testing. In: ICTSS (2012). https://doi.org/10.1007/978-3-642-34691-0_10

  5. Bannour, B., Lapitre, A., Le Gall, P., Nguyen, T.: Symbolic path-guided test cases for models with data and time, version of this paper extended with appendix (2023). https://doi.org/10.48550/ar**v.2309.06840

  6. Benharrat, N., Gaston, C., Hierons, R.M., Lapitre, A., Le Gall, P.: Constraint-based oracles for timed distributed systems. In: Yevtushenko, N., Cavalli, A.R., Yenigün, H. (eds.) ICTSS 2017. LNCS, vol. 10533, pp. 276–292. Springer, Cham (2017). https://doi.org/10.1007/978-3-319-67549-7_17

    Chapter  Google Scholar 

  7. de Boer, F.S., Bonsangue, M.: On the nature of symbolic execution. In: ter Beek, M.H., McIver, A., Oliveira, J.N. (eds.) FM 2019. LNCS, vol. 11800, pp. 64–80. Springer, Cham (2019). https://doi.org/10.1007/978-3-030-30942-8_6

    Chapter  Google Scholar 

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

  9. CEA: diversity, eclipse formal modeling project. https://projects.eclipse.org/proposals/eclipse-formal-modeling-project (2023)

  10. 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). https://doi.org/10.1007/978-3-540-78800-3_24

    Chapter  Google Scholar 

  11. Escobedo, J.P., Gaston, C., Gall, P.L., Cavalli, A.R.: Testing web service orchestrators in context: a symbolic approach. In: SEFM, pp. 257–267. IEEE Computer Society (2010)

    Google Scholar 

  12. Frantzen, L., Tretmans, J., Willemse, T.A.C.: Test generation based on symbolic specifications. In: FATES (2004). https://doi.org/10.1007/978-3-540-31848-4_1

  13. 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). https://doi.org/10.1007/11940197_3

    Chapter  Google Scholar 

  14. Gaston, C., Hierons, R.M., Le Gall, P.: An implementation relation and test framework for timed distributed systems. In: ICTSS (2013). https://doi.org/10.1007/978-3-642-41707-8_6

  15. Gaston, C., Le Gall, P., Rapin, N., Touil, A.: Symbolic execution techniques for test purpose definition. In: TestCom (2006). https://doi.org/10.1007/11754008_1

  16. Henry, L., Jéron, T., Markey, N.: Control strategies for off-line testing of timed systems. Formal Methods Syst. Des. (2022). https://doi.org/10.1007/s10703-022-00403-w

    Article  Google Scholar 

  17. Hessel, A., Larsen, K.G., Mikucionis, M., Nielsen, B., Pettersson, P., Skou, A.: Testing real-time systems using UPPAAL. In: FORTEST (2008). https://doi.org/10.1007/978-3-540-78917-8_3

  18. Janssen, R., Tretmans, J.: Matching implementations to specifications: the corner cases of ioco. In: Hung, C., Papadopoulos, G.A. (eds.) SAC. ACM (2019). https://doi.org/10.1145/3297280.3297496

  19. Jéron, T.: Symbolic model-based test selection. In: Machado, P.D.L. (ed.) SBMF. Elsevier (2008). https://doi.org/10.1016/j.entcs.2009.05.051

  20. King, J.C.: Symbolic execution and program testing. Commun. ACM 19(7), 385–394 (1976)

    Article  MathSciNet  Google Scholar 

  21. 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). https://doi.org/10.1007/978-3-540-24732-6_8

    Chapter  Google Scholar 

  22. Krichen, M., Tripakis, S.: Interesting properties of the real-time conformance relation tioco. In: Barkaoui, K., Cavalcanti, A., Cerone, A. (eds.) ICTAC 2006. LNCS, vol. 4281, pp. 317–331. Springer, Heidelberg (2006). https://doi.org/10.1007/11921240_22

    Chapter  Google Scholar 

  23. Luthmann, L., Göttmann, H., Lochau, M.: Compositional liveness-preserving conformance testing of timed I/O automata. In: Arbab, F., Jongmans, S.-S. (eds.) FACS 2019. LNCS, vol. 12018, pp. 147–169. Springer, Cham (2020). https://doi.org/10.1007/978-3-030-40914-2_8

    Chapter  Google Scholar 

  24. Marsso, L., Mateescu, R., Serwe, W.: TESTOR: a modular tool for on-the-fly conformance test case generation. In: Beyer, D., Huisman, M. (eds.) TACAS 2018. LNCS, vol. 10806, pp. 211–228. Springer, Cham (2018). https://doi.org/10.1007/978-3-319-89963-3_13

    Chapter  Google Scholar 

  25. Rusu, V., Marchand, H., Jéron, T.: Automatic verification and conformance testing for validating safety properties of reactive systems. In: Fitzgerald, J., Hayes, I.J., Tarlecki, A. (eds.) FM 2005. LNCS, vol. 3582, pp. 189–204. Springer, Heidelberg (2005). https://doi.org/10.1007/11526841_14

    Chapter  Google Scholar 

  26. Standard, E.: Methods for testing and specification (MTS); the testing and test control notation version 3; Part 1: TTCN-3 core language (2005)

    Google Scholar 

  27. von Styp, S., Bohnenkamp, H., Schmaltz, J.: A conformance testing relation for symbolic timed automata. In: Chatterjee, K., Henzinger, T.A. (eds.) FORMATS 2010. LNCS, vol. 6246, pp. 243–255. Springer, Heidelberg (2010). https://doi.org/10.1007/978-3-642-15297-9_19

    Chapter  Google Scholar 

  28. 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). https://doi.org/10.1007/3-540-61042-1_42

    Chapter  Google Scholar 

  29. Tretmans, J., Janssen, R.: Goodbye ioco. In: a journey from process algebra via timed automata to model learning. Springer, Cham (2022). https://doi.org/10.1007/978-3-031-15629-8_26

Download references

Author information

Authors and Affiliations

  1. Université Paris-Saclay, CEA, List, 91120, Palaiseau, France

    Boutheina Bannour & Arnault Lapitre

  2. Université Paris-Saclay, CentraleSupélec, MICS, 91192, Gif-sur-Yvette, France

    Pascale Le Gall & Thang Nguyen

Authors
  1. Boutheina Bannour
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Arnault Lapitre
    View author publications

    You can also search for this author in PubMed Google Scholar

  3. Pascale Le Gall
    View author publications

    You can also search for this author in PubMed Google Scholar

  4. Thang Nguyen
    View author publications

    You can also search for this author in PubMed Google Scholar

Corresponding author

Correspondence to Boutheina Bannour .

Editor information

Editors and Affiliations

  1. University of Malaga, Málaga, Spain

    Javier Cámara

  2. Open University of Netherlands, Heerlen, The Netherlands

    Sung-Shik Jongmans

Rights and permissions

Reprints and permissions

Copyright information

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

About this paper

Check for updates. Verify currency and authenticity via CrossMark

Cite this paper

Bannour, B., Lapitre, A., Gall, P.L., Nguyen, T. (2024). Symbolic Path-Guided Test Cases for Models with Data and Time. In: Cámara, J., Jongmans, SS. (eds) Formal Aspects of Component Software. FACS 2023. Lecture Notes in Computer Science, vol 14485. Springer, Cham. https://doi.org/10.1007/978-3-031-52183-6_1

Download citation

  • DOI: https://doi.org/10.1007/978-3-031-52183-6_1

  • Published:

  • Publisher Name: Springer, Cham

  • Print ISBN: 978-3-031-52182-9

  • Online ISBN: 978-3-031-52183-6

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation