Top

Published in:

2024 | OriginalPaper | Chapter

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

Authors : Boutheina Bannour, Arnault Lapitre, Pascale Le Gall, Thang Nguyen

Published in: Formal Aspects of Component Software

Publisher: Springer Nature Switzerland

Activate our intelligent search to find suitable subject content or patents.

search-config

AI-assisted search

Off

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.

Dont have a licence yet? Then find out more about our products and how to get one now:

Springer Professional "Wirtschaft+Technik"

Online-Abonnement

Mit Springer Professional "Wirtschaft+Technik" erhalten Sie Zugriff auf:

über 102.000 Bücher
über 537 Zeitschriften

aus folgenden Fachgebieten:

Automobil + Motoren
Bauwesen + Immobilien
Business IT + Informatik
Elektrotechnik + Elektronik
Energie + Nachhaltigkeit
Finance + Banking
Management + Führung
Marketing + Vertrieb
Maschinenbau + Werkstoffe
Versicherung + Risiko

Jetzt Wissensvorsprung sichern!

inform now

Springer Professional "Technik"

Online-Abonnement

Mit Springer Professional "Technik" erhalten Sie Zugriff auf:

über 67.000 Bücher
über 390 Zeitschriften

aus folgenden Fachgebieten:

Automobil + Motoren
Bauwesen + Immobilien
Business IT + Informatik
Elektrotechnik + Elektronik
Energie + Nachhaltigkeit
Maschinenbau + Werkstoffe

Jetzt Wissensvorsprung sichern!

inform now

Springer Professional "Wirtschaft"

Online-Abonnement

Mit Springer Professional "Wirtschaft" erhalten Sie Zugriff auf:

über 67.000 Bücher
über 340 Zeitschriften

aus folgenden Fachgebieten:

Bauwesen + Immobilien
Business IT + Informatik
Finance + Banking
Management + Führung
Marketing + Vertrieb
Versicherung + Risiko

Jetzt Wissensvorsprung sichern!

inform now

next chapter Model-Based Testing of Asynchronously Communicating Distributed Controllers

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

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

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

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

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

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

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/arXiv.2309.06840

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_17CrossRef

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_6CrossRef

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_5CrossRef

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_24CrossRef

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)

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_3CrossRef

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-wCrossRef

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)MathSciNetCrossRef

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_8CrossRef

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_22CrossRef

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_8CrossRef

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_13CrossRef

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_14CrossRef

26.

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

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_19CrossRef

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_42CrossRef

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

Title: Symbolic Path-Guided Test Cases for Models with Data and Time
Authors: Boutheina Bannour
Arnault Lapitre
Pascale Le Gall
Thang Nguyen
Publisher: Springer Nature Switzerland
Book: Formal Aspects of Component Software
Print ISBN: 978-3-031-52182-9

Electronic ISBN: 978-3-031-52183-6

Copyright Year: 2024
DOI: https://doi.org/10.1007/978-3-031-52183-6_1

Springer Professional

Abstract

Please log in to get access to your license.

Dont have a licence yet? Then find out more about our products and how to get one now:

Springer Professional "Wirtschaft+Technik"

Springer Professional "Technik"

Springer Professional "Wirtschaft"

Premium Partner