publication . Conference object . Article . Part of book or chapter of book . 2017

Symbolic execution of transition systems with function summaries

Boudhiba , I.; Gaston , C.; Le Gall , P.; Prevosto , V.;
Open Access English
  • Published: 19 Jul 2017
  • Publisher: HAL CCSD
  • Country: France
Abstract
Conference of 11th International Conference on Tests and Proofs, TAP 2017, held as part of STAF 2017 ; Conference Date: 19 July 2017 Through 20 July 2017; Conference Code:194199; International audience; 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...
Subjects
free text keywords: Functions summaries, Symbolic Execution, Transition coverage, Input Output Symbolic Transition Systems, Functions sum- maries, [INFO]Computer Science [cs], Artificial intelligence, Computer science, Computers, Function summaries, Input/output datum, Logical formulas, Numerical inputs, Symbolic Transition Systems, Transition system, Model checking, [ INFO ] Computer Science [cs], Input/output, Automaton, Programming language, computer.software_genre, computer, Test case, Reactive system, Theoretical computer science, Tuple
Funded by
EC| VESSEDIA
Project
VESSEDIA
VERIFICATION ENGINEERING OF SAFETY AND SECURITY CRITICAL DYNAMIC INDUSTRIAL APPLICATIONS
  • Funder: European Commission (EC)
  • Project Code: 731453
  • Funding stream: H2020 | RIA
36 references, page 1 of 3

1. Saswat Anand, Patrice Godefroid, and Nikolai Tillmann. Demand-driven compositional symbolic execution. In Proceedings of the Theory and Practice of Software, 14th International Conference on Tools and Algorithms for the Construction and Analysis of Systems, pages 367{381, Berlin, Heidelberg, 2008. Springer-Verlag.

2. Saswat Anand, Corina S. Pasareanu, and Willem Visser. Jpf-se: A symbolic execution extension to java path nder. In Proceedings of the 13th International Conference on Tools and Algorithms for the Construction and Analysis of Systems, pages 134{138, Berlin, Heidelberg, 2007. Springer-Verlag.

3. Mathilde Arnaud, Boutheina Bannour, and Arnault Lapitre. An illustrative use case of the diversity platform based on uml interaction scenarios. Electron. Notes Theor. Comput. Sci., pages 21{34, 2016.

4. Domagoj Babic and Alan J. Hu. Structural abstraction of software veri cation conditions. In Proceedings of the 19th International Conference on Computer Aided Veri cation, pages 366{378, Berlin, Heidelberg, 2007. Springer-Verlag. [OpenAIRE]

5. Boutheina Bannour, Jose Pablo Escobedo, Christophe Gaston, and Pascale Le Gall. O -line test case generation for timed symbolic model-based conformance testing. In Testing Software and Systems, pages 119{135. Springer, 2012.

6. Boutheina Bannour, Christophe Gaston, Marc Aiguier, and Arnault Lapitre. Results for compositional timed testing. In 20th Asia-Paci c Software Engineering Conference, APSEC, pages 559{564. IEEE Computer Society, 2013.

7. N. Bj rner, N. Tillmann, and A. Voronkov. Path feasibility analysis for stringmanipulating programs. In TACAS, volume 5505 of LNCS. Springer, 2009.

8. Imen Boudhiba, Christophe Gaston, Pascale Le Gall, and Virgile Prevosto. Modelbased testing from input output symbolic transition systems enriched by program calls and contracts. In Testing Software and Systems - 27th IFIP WG 6.1 International Conference, ICTSS, volume 9447 of Lecture Notes in Computer Science, pages 35{51. Springer, 2015.

9. Cristian Cadar and Dawson Engler. Execution generated test cases: How to make systems code crash itself. Software Model Checking (SPIN), 2005.

10. James C.King. Symbolic execution and program testing. Communication ACM, 19:385{394, 1976.

11. Lori A Clarke. A system to generate test data and symbolically execute programs. IEEE Trans. Softw. Eng., pages 215{222, 1976.

12. The consortium Sesam-Grids. The Sesam-Grids Project. In http://www.sesamgrids.org/.

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

14. J. Deltour, A. Faivre, E. Gaudin, and A. Lapitre. Model-based testing: An approach with SDL/RTDS and DIVERSITY. In SAM, volume 8769 of LNCS. Springer, 2014. [OpenAIRE]

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

36 references, page 1 of 3
Powered by OpenAIRE Open Research Graph
Any information missing or wrong?Report an Issue
publication . Conference object . Article . Part of book or chapter of book . 2017

Symbolic execution of transition systems with function summaries

Boudhiba , I.; Gaston , C.; Le Gall , P.; Prevosto , V.;