Advertisement

Checking Sequence Generation for Symbolic Input/Output FSMs by Constraint Solving

  • Omer Nguena Timo
  • Alexandre Petrenko
  • S. Ramesh
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 11187)

Abstract

The reset of reactive systems in testing can be impossible or very costly, which could force testers to avoid it. In this context, testers often want to generate a checking sequence, i.e., a unique sequence of inputs satisfying a chosen test criterion. This paper proposes a method for generating a checking sequence with complete fault coverage for a given fault model of reactive systems. The systems are represented with an extension of Finite State Machines (FSMs) with symbolic inputs and outputs which are predicates on input and output variables having possibly infinite domains. In our setting, a checking sequence is made up of symbolic inputs and the fault domain can represent complex faults. The method consists in building and solving Boolean expressions to iteratively refine and extend a sequence of symbolic inputs. We evaluate the efficiency of the approach with a prototype tool we have developed.

Keywords

Extended FSM Symbolic input/output FSM Checking sequence Fault modeling Fault detection Constraint solving 

Notes

Acknowledgment

This work is supported in part by GM, NSERC of Canada and MESI (Ministère de l’Économie, Science et Innovation) of Gouvernement du Québec.

References

  1. 1.
    Androutsopoulos, K., Clark, D., Harman, M., Hierons, R.M., Li, Z., Tratt, L.: Amorphous slicing of extended finite state machines. IEEE Trans. Softw. Eng. 39(7), 892–909 (2013).  https://doi.org/10.1109/tse.2012.72CrossRefGoogle Scholar
  2. 2.
    Bessayah, F., Cavalli, A., Maja, W., Martins, E., Valenti, A.W.: A fault injection tool for testing web services composition. In: Bottaci, L., Fraser, G. (eds.) TAIC PART 2010. LNCS, vol. 6303, pp. 137–146. Springer, Heidelberg (2010).  https://doi.org/10.1007/978-3-642-15585-7_13CrossRefGoogle Scholar
  3. 3.
    Delamaro, M.E., Maldonado, J.C., Pasquini, A., Mathur, A.P.: Interface mutation test adequacy criterion: an empirical evaluation. Empir. Softw. Eng. 6(2), 111–142 (2001).  https://doi.org/10.1023/a:1011429104252CrossRefzbMATHGoogle Scholar
  4. 4.
    Eén, N., Sörensson, N.: An extensible SAT-solver. In: Giunchiglia, E., Tacchella, A. (eds.) SAT 2003. LNCS, vol. 2919, pp. 502–518. Springer, Heidelberg (2004).  https://doi.org/10.1007/978-3-540-24605-3_37CrossRefGoogle Scholar
  5. 5.
    Godefroid, P., Klarlund, N., Sen, K.: DART: directed automated random testing. ACM SIGPLAN Not. 40(6), 213–223 (2005).  https://doi.org/10.1145/1064978.1065036CrossRefGoogle Scholar
  6. 6.
    Hennie, F.C.: Fault detecting experiments for sequential circuits. In: Proceedings of 5th Annual Symposium on Switching Circuit Theory and Logical Design, SWCT 1964, November 1964, Princeton, NJ, pp. 95–110. IEEE CS Press, Washington, DC (1964).  https://doi.org/10.1109/swct.1964.8
  7. 7.
    Hierons, R.M., Jourdan, G.V., Ural, H., Yenigun, H.: Checking sequence construction using adaptive and preset distinguishing sequences. In: Proceedings of 7th IEEE International Conference on Software Engineering and Formal Methods, SEFM 2009, November 2009, Hanoi, pp. 157–166. IEEE CS Press, Washington (2009).  https://doi.org/10.1109/sefm.2009.12
  8. 8.
    Jia, Y., Harman, M.: An analysis and survey of the development of mutation testing. IEEE Trans. Softw. Eng. 37(5), 649–678 (2011).  https://doi.org/10.1109/tse.2010.62CrossRefGoogle Scholar
  9. 9.
    Jourdan, G.V., Ural, H., Yenigün, H.: Reducing locating sequences for testing from finite state machines. In: Proceedings of 31st Annual ACM Symposium on Applied Computing, SAC 2016, April 2016, Pisa, pp. 1654–1659. ACM, New York (2016).  https://doi.org/10.1145/2851613.2851831
  10. 10.
    Koufareva, I., Petrenko, A., Yevtushenko, N.: Test generation driven by user-defined fault models. In: Csopaki, G., Dibuz, S., Tarnay, K. (eds.) Testing of Communicating Systems. ITIFIP, vol. 21, pp. 215–233. Springer, Boston, MA (1999).  https://doi.org/10.1007/978-0-387-35567-2_14CrossRefGoogle Scholar
  11. 11.
    Moore, E.F.: Gedanken-experiments on sequential machines. In: Shannon, C., McCarthy, J. (eds.) Automata Studies, pp. 129–153. Princeton University Press, Princeton (1956)Google Scholar
  12. 12.
    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_24CrossRefGoogle Scholar
  13. 13.
    Nguena Timo, O., Petrenko, A., Ramesh, S.: Multiple mutation testing from finite state machines with symbolic inputs. In: Yevtushenko, N., Cavalli, A.R., Yenigün, H. (eds.) ICTSS 2017. LNCS, vol. 10533, pp. 108–125. Springer, Cham (2017).  https://doi.org/10.1007/978-3-319-67549-7_7CrossRefGoogle Scholar
  14. 14.
    Parr, T.: The Definitive ANTLR 4 Reference, 2nd edn. Pragmatic Bookshelf, Dallas and Raleigh (2013)Google Scholar
  15. 15.
    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).  https://doi.org/10.1007/3-540-45510-8_10CrossRefGoogle Scholar
  16. 16.
    Petrenko, A.: Toward testing from finite state machines with symbolic inputs and outputs. Softw. Syst. Model. (2017, to appear).  https://doi.org/10.1007/s10270-017-0613-x
  17. 17.
    Petrenko, A., Avellaneda, F., Groz, R., Oriat, C.: From passive to active FSM inference via checking sequence construction. In: Yevtushenko, N., Cavalli, A.R., Yenigün, H. (eds.) ICTSS 2017. LNCS, vol. 10533, pp. 126–141. Springer, Cham (2017).  https://doi.org/10.1007/978-3-319-67549-7_8CrossRefGoogle Scholar
  18. 18.
    Petrenko, A., Boroday, S., Groz, R.: Confirming configurations in EFSM testing. IEEE Trans. Softw. Eng. 30(1), 29–42 (2004).  https://doi.org/10.1109/tse.2004.1265734CrossRefzbMATHGoogle Scholar
  19. 19.
    Petrenko, A., Dury, A., Ramesh, S., Mohalik, S.: A method and tool for test optimization for automotive controllers. In: Workshops Proceedings of 6th IEEE International Conference on Software Testing, Verification and Validation, ICST 2013 Workshops, March 2013, Luxembourg, pp. 198–207. IEEE CS Press, Washington, DC (2013).  https://doi.org/10.1109/icstw.2013.31
  20. 20.
    Petrenko, A., Nguena Timo, O., Ramesh, S.: Multiple mutation testing from FSM. In: Albert, E., Lanese, I. (eds.) FORTE 2016. LNCS, vol. 9688, pp. 222–238. Springer, Cham (2016).  https://doi.org/10.1007/978-3-319-39570-8_15CrossRefGoogle Scholar
  21. 21.
    Petrenko, A., Nguena Timo, O., Ramesh, S.: Test generation by constraint solving and FSM mutant killing. In: Wotawa, F., Nica, M., Kushik, N. (eds.) ICTSS 2016. LNCS, vol. 9976, pp. 36–51. Springer, Cham (2016).  https://doi.org/10.1007/978-3-319-47443-4_3CrossRefzbMATHGoogle Scholar
  22. 22.
    Petrenko, A., Simao, A.: Generating checking sequences for user defined fault models. In: Yevtushenko, N., Cavalli, A.R., Yenigün, H. (eds.) ICTSS 2017. LNCS, vol. 10533, pp. 320–325. Springer, Cham (2017).  https://doi.org/10.1007/978-3-319-67549-7_20CrossRefGoogle Scholar
  23. 23.
    Petrenko, A., Simao, A.: Checking experiments for finite state machines with symbolic inputs. In: El-Fakih, K., Barlas, G., Yevtushenko, N. (eds.) ICTSS 2015. LNCS, vol. 9447, pp. 3–18. Springer, Cham (2015).  https://doi.org/10.1007/978-3-319-25945-1_1CrossRefGoogle Scholar
  24. 24.
    Petrenko, A., Yevtushenko, N.: Test suite generation from a FSM with a given type of implementation errors. In: Linn Jr., R.J., Uyar, M.Ü. (eds.) Proceedings of IFIP TC6/WG6.1 12th International Symposium on Protocol Specification, Testing and Verification, Lake Buena Vista, FL, June 1992. IFIP Transactions C: Communication Systems, vol. 8, pp. 229–243. North-Holland, Amsterdam (1992).  https://doi.org/10.1016/b978-0-444-89874-6.50021-0CrossRefGoogle Scholar
  25. 25.
    Thummalapenta, S., Xie, T., Tillmann, N., de Halleux, J., Su, Z.: Synthesizing method sequences for high-coverage testing. ACM SIGPLAN Not. 46(10), 189–206 (2011).  https://doi.org/10.1145/2076021.2048083CrossRefGoogle Scholar
  26. 26.
    Utting, M., Pretschner, A., Legeard, B.: A taxonomy of model-based testing approaches. Softw. Test. Verif. Reliab. 22(5), 297–312 (2012).  https://doi.org/10.1002/stvr.456CrossRefGoogle Scholar
  27. 27.
    Yannakakis, M., Lee, D.: Testing finite state machines: fault detection. J. Comput. Syst. Sci. 50(2), 209–227 (1995).  https://doi.org/10.1006/jcss.1995.1019MathSciNetCrossRefzbMATHGoogle Scholar
  28. 28.
    Zhu, H., Hall, P.A.V., May, J.H.R.: Software unit test coverage and adequacy. ACM Comput. Surv. 29(4), 366–427 (1997).  https://doi.org/10.1145/267580.267590CrossRefGoogle Scholar

Copyright information

© Springer Nature Switzerland AG 2018

Authors and Affiliations

  • Omer Nguena Timo
    • 1
  • Alexandre Petrenko
    • 1
  • S. Ramesh
    • 2
  1. 1.Computer Research Institute of Montreal, CRIMMontrealCanada
  2. 2.GM Global R&DWarrenUSA

Personalised recommendations