Skip to main content
SpringerLink
Log in
Book cover

International Conference on Tests and Proofs

TAP 2017: Tests and Proofs pp 41–58Cite as

Symbolic Execution of Transition Systems with Function Summaries

  • Conference paper
  • First Online:

  • 608 Accesses

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

Abstract

Reactive systems can be modeled with various kinds of automata, such as Input Output Symbolic Transition Systems (IOSTS). Symbolic execution (SE) applied to IOSTS allows computing constraints associated to IOSTS path executions (path conditions). In this context, generating test cases amounts to finding numerical input values satisfying such constraints using solvers. This paper explores the case where IOSTS models contain functions which are outside of the scope of such solvers. We propose to use function summaries which are logical formulas built from concrete values describing some representative input/output data tuples of the function. We define algorithmic strategies to solve path conditions including such functions based on techniques using and enriching function summaries. Our method has been implemented within the Diversity tool and has been applied to several examples.

Part of this work has been conducted within the French PIA project SESAM Grids 2012–2016 [12] and the Vessedia project funded from European Union’s Horizon 2020 research and innovation programme under grant agreement No. 731453.

This is a preview of subscription content, 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

Learn about institutional subscriptions

Notes

  1. 1.

    A constant is a function of profile of the form \(\rightarrow s\).

  2. 2.

    For a couple \(c = (e,f)\) of elements, \(c_{|1}\) is e and \(c_{|2}\) is f.

  3. 3.

    https://projects.eclipse.org/proposals/eclipse-formal-modeling-project.

  4. 4.

    https://z3.codeplex.com/.

  5. 5.

    http://cvc4.cs.nyu.edu/web/.

References

  1. Anand, S., Godefroid, P., Tillmann, N.: Demand-driven compositional symbolic execution. In: Ramakrishnan, C.R., Rehof, J. (eds.) TACAS 2008. LNCS, vol. 4963, pp. 367–381. Springer, Heidelberg (2008). doi:10.1007/978-3-540-78800-3_28

    Chapter  Google Scholar 

  2. Anand, S., Păsăreanu, C.S., Visser, W.: JPF–SE: a symbolic execution extension to Java PathFinder. In: Grumberg, O., Huth, M. (eds.) TACAS 2007. LNCS, vol. 4424, pp. 134–138. Springer, Heidelberg (2007). doi:10.1007/978-3-540-71209-1_12

    Chapter  Google Scholar 

  3. Arnaud, M., Bannour, B., Lapitre, A.: An illustrative use case of the DIVERSITY Platform based on UML interaction scenarios. Electron. Notes Theor. Comput. Sci. 320, 21–34 (2016)

    Article  MathSciNet  Google Scholar 

  4. Babić, D., Hu, A.J.: Structural abstraction of software verification conditions. In: Damm, W., Hermanns, H. (eds.) CAV 2007. LNCS, vol. 4590, pp. 366–378. Springer, Heidelberg (2007). doi:10.1007/978-3-540-73368-3_41

    Chapter  Google Scholar 

  5. Bannour, B., Escobedo, J.P., Gaston, C., Le Gall, P.: Off-line test case generation for timed symbolic model-based conformance testing. In: Nielsen, B., Weise, C. (eds.) ICTSS 2012. LNCS, vol. 7641, pp. 119–135. Springer, Heidelberg (2012). doi:10.1007/978-3-642-34691-0_10

    Chapter  Google Scholar 

  6. Bannour, B., Gaston, C., Aiguier, M., Lapitre, A.: Results for compositional timed testing. In: 20th Asia-Pacific Software Engineering Conference, APSEC, pp. 559–564. IEEE Computer Society (2013)

    Google Scholar 

  7. Bjørner, N., Tillmann, N., Voronkov, A.: Path feasibility analysis for string-manipulating programs. In: Kowalewski, S., Philippou, A. (eds.) TACAS 2009. LNCS, vol. 5505, pp. 307–321. Springer, Heidelberg (2009). doi:10.1007/978-3-642-00768-2_27

    Chapter  Google Scholar 

  8. Boudhiba, I., Gaston, C., Le Gall, P., Prevosto, V.: Model-based testing from input output symbolic transition systems enriched by program calls and contracts. In: El-Fakih, K., Barlas, G., Yevtushenko, N. (eds.) ICTSS 2015. LNCS, vol. 9447, pp. 35–51. Springer, Cham (2015). doi:10.1007/978-3-319-25945-1_3

    Chapter  Google Scholar 

  9. Cadar, C., Engler, D.: Execution generated test cases: how to make systems code crash itself. In: Godefroid, P. (ed.) SPIN 2005. LNCS, vol. 3639, pp. 2–23. Springer, Heidelberg (2005). doi:10.1007/11537328_2

    Chapter  Google Scholar 

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

    Article  MathSciNet  MATH  Google Scholar 

  11. Clarke, L.A.: A system to generate test data and symbolically execute programs. IEEE Trans. Softw. Eng. 3, 215–222 (1976)

    Article  MathSciNet  Google Scholar 

  12. The Consortium Sesam-Grids: The Sesam-Grids Project. http://www.sesam-grids.org/

  13. CREST. https://code.google.com/archive/p/crest/. Accessed 04 Mar 2017

  14. Deltour, J., Faivre, A., Gaudin, E., Lapitre, A.: Model-based testing: an approach with SDL/RTDS and DIVERSITY. In: Amyot, D., Fonseca i Casas, P., Mussbacher, G. (eds.) SAM 2014. LNCS, vol. 8769, pp. 198–206. Springer, Cham (2014). doi:10.1007/978-3-319-11743-0_14

    Google Scholar 

  15. DIVERSITY. https://projects.eclipse.org/proposals/eclipse-formal-modeling-project. Accessed 04 Mar 2017

  16. Engler, D., Dunbar, D.: Under-constrained execution: making automatic code destruction easy and scalable. In: Proceedings of the 2007 International Symposium on Software Testing and Analysis, pp. 1–4. ACM, New York (2007)

    Google Scholar 

  17. Gaston, C., Le Gall, P., Rapin, N., Touil, A.: Symbolic execution techniques for test purpose definition. In: Uyar, M.Ü., Duale, A.Y., Fecko, M.A. (eds.) TestCom 2006. LNCS, vol. 3964, pp. 1–18. Springer, Heidelberg (2006). doi:10.1007/11754008_1

    Chapter  Google Scholar 

  18. Godefroid, P., Klarlund, N., Sen, K.: Dart: directed automated random testing. In: Proceedings of the 2005 ACM SIGPLAN Conference on Programming Language Design and Implementation, PLDI 2005, pp. 213–223 (2005)

    Google Scholar 

  19. Gopan, D., Reps, T.: Low-level library analysis and summarization. In: Damm, W., Hermanns, H. (eds.) CAV 2007. LNCS, vol. 4590, pp. 68–81. Springer, Heidelberg (2007). doi:10.1007/978-3-540-73368-3_10

    Chapter  Google Scholar 

  20. jCUTE. http://osl.cs.illinois.edu/software/jcute/. Accessed 04 Mar 2017

  21. Khurshid, S., Suen, Y.L.: Generalizing symbolic execution to library classes. SIGSOFT Softw. Eng. Notes 31, 103–110 (2005)

    Article  Google Scholar 

  22. Kicillof, N., Grieskamp, W., Tillmann, N., Braberman, V.: Achieving both model and code coverage with automated gray-box testing. In: Advances in Model-Based Testing (A-MOST). ACM (2007)

    Google Scholar 

  23. MathWorks: The Simulink documentation. http://fr.mathworks.com/help/simulink/

  24. Mouy, P., Marre, B., Willams, N., Le Gall, P.: Generation of all-paths unit test with function calls. In: International Conference on Software Testing (ICST), pp. 32–41 (2008)

    Google Scholar 

  25. Myers, G.J., Sandlers, C., Badgett, T.: The Art of Software Testing, 3rd edn. Wiley, New York (2011)

    Google Scholar 

  26. Object Management Group: The UML standard specification. http://www.omg.org/spec/UML/2.4.1/

  27. PathCrawler. http://frama-c.com/pathcrawler.html. Accessed 04 Mar 2017

  28. Symbolic PathFinder. http://babelfish.arc.nasa.gov/trac/jpf/wiki/projects/jpf-symbc. Accessed 04 Mar 2017

  29. Păsăreanu, C.S., Rungta, N., Visser, W.: Symbolic execution with mixed concrete-symbolic solving. In: Proceedings of the 2011 International Symposium on Software Testing and Analysis, pp. 34–44. ACM, New York (2011)

    Google Scholar 

  30. Rutten, J.J.M.M.: A calculus of transition systems (towards universal coalgebra). Technical report, CWI (Centre for Mathematics and Computer Science), Amsterdam, The Netherlands (1995)

    Google Scholar 

  31. Sen, K., Marinov, D., Agha, G.: CUTE: a concolic unit testing engine for C. SIGSOFT Softw. Eng. Notes 30, 263–272 (2005)

    Article  Google Scholar 

  32. Tretmans, J.: Conformance testing with labelled transition systems: implementation relations and test generation. Comput. Netw. ISDN Syst. 29(1), 49–79 (1996)

    Article  Google Scholar 

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

  34. Wang, Y., Xing, Y., Zhang, X.: A method of path feasibility judgment based on symbolic execution and range analysis. Int. J. Future Gener. Commun. Netw. 7, 205–212 (2014)

    Article  Google Scholar 

  35. Williams, N., Marre, B., Mouy, P., Roger, M.: PathCrawler: automatic generation of path tests by combining static and dynamic analysis. In: Dal Cin, M., Kaâniche, M., Pataricza, A. (eds.) EDCC 2005. LNCS, vol. 3463, pp. 281–292. Springer, Heidelberg (2005). doi:10.1007/11408901_21

    Chapter  Google Scholar 

Download references

Author information

Authors and Affiliations

  1. Laboratoire MICS, Grande Voie des Vignes, 92195, Châtenay-malabry, France

    Imen Boudhiba & Pascale Le Gall

  2. CEA LIST, Point Courrier 174, 91191, Gif-sur-Yvette, France

    Christophe Gaston & Virgile Prevosto

Authors
  1. Imen Boudhiba
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Christophe Gaston
    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. Virgile Prevosto
    View author publications

    You can also search for this author in PubMed Google Scholar

Corresponding author

Correspondence to Imen Boudhiba .

Editor information

Editors and Affiliations

  1. Technical University of Darmstadt, Darmstadt, Germany

    Sebastian Gabmeyer

  2. University of Oslo, Oslo, Norway

    Einar Broch Johnsen

Rights and permissions

Reprints and permissions

Copyright information

© 2017 Springer International Publishing AG

About this paper

Cite this paper

Boudhiba, I., Gaston, C., Gall, P.L., Prevosto, V. (2017). Symbolic Execution of Transition Systems with Function Summaries. In: Gabmeyer, S., Johnsen, E. (eds) Tests and Proofs. TAP 2017. Lecture Notes in Computer Science(), vol 10375. Springer, Cham. https://doi.org/10.1007/978-3-319-61467-0_3

Download citation

  • DOI: https://doi.org/10.1007/978-3-319-61467-0_3

  • Published:

  • Publisher Name: Springer, Cham

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

  • Online ISBN: 978-3-319-61467-0

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation