Dynamic analysis of programs with graphical user interface based on symbolic execution

In this paper, we explore the possibilities of applying dynamic symbolic execution (or concolic testing) methods to applications with graphical user interfaces. Such applications inherently feature interactive user input processing and multithreaded execution. These features typically decrease the effectiveness of dynamic symbolic execution by increasing the volume of processed code not related to actual application functionality. We present a hybrid approach that combines commonly used GUI test automation methods based on GUI model excavation with dynamic symbolic execution methods to construct test cases for checking internal application logic. We have implemented this approach using two open-source tools - test automation framework GUITAR and Java byte-code static instrumentation framework Coffee Machine. GUI model extracted automatically by GUITAR tool is extended with symbolic traces relevant to application GUI event handlers. Our test generation module for GUITAR combines these symbolic traces into complex queries to be processed by SMT solver. The resulting test cases are valid within automatically extracted GUI structure model and allow to check different execution paths in GUI event handler code. We have checked our hybrid approach on a set of small open-source applications and identified several bugs caused by uncaught exceptions. The paper is concluded with an overview of current limitations and possible improvements of the hybrid approach.

dynamic analysis, program analysis, GUI testing, test coverage

1. Mobile Banking Rank 2015 (http://markswebb.ru/e-finance/internet-banking-rank-2015/)

2. Ranorex. http://www.ranorex.com/ [HTML]. Accessed at 10.10.2016

3. Abbot framework for automated testing of Java GUI components and programs. https://abbot.sourceforge.net. Accessed at 10.10.2016

4. Maveryx. https://sourceforge.net/projects/maveryx/ [HTML]. Обращение от 10.10.2016

5. Squish: https://www.froglogic.com/squish/ [HTML]. Обращение от 10.10.2016

6. Sikuli: using GUI screenshots for search automation. UIST’09 Proceedings of the 22nd annual ACM symposium on User Interface software and technology. Victoria, BC, Canada. Octomer 04-07, 2009. pp. 183-192

7. Bao N. Nguyen, Bryan Robbins, Ishan Banerjee, Atif Memon. GUITAR: an innovative tool for automated testing of GUI-driven software. Automated software engineering. - 2013. - Vol. 21(1). pp. 65-105.

8. Willem Visser, Corina S. Pāsāreanu, Sarfranz Khurshid. Test input generation with java PathFinder. ISSTA '04 Proceedings of the 2004 ACM SIGSOFT international symposium on Software testing and analysis. Boston, Massachusetts, USA. July 11-14, 2004. pp. 97-107.

9. Gary Lindstrom, Peter C. Mahlitz, Willem Visser. Model checking real time java using java pathfinder. Proceeding ATVA’05 Proceedings of the Third international conference on Automated Technology for Verification and Analysis. Taipei, Taiwan. October 04-07, 2005. pp. 444-456.

10. Howar, Falk, Malte Isberner, Temesghen Kahsai, Zvonimir Rakamaric, and Vishwanath Raman. "JDART: A Dynamic Symbolic Analysis Framework." In Tools and Algorithms for the Construction and Analysis of Systems: 22nd International Conference, TACAS 2016, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2016, Eindhoven, The Netherlands, April 2-8, 2016, Proceedings, vol. 9636, Springer, 2016. p. 442.

11. Farzan A, Chen F, Meseguer J, Roşu G. Formal analysis of Java programs in JavaFAN. InInternational Conference on Computer Aided Verification 2004 Jul 13. Springer Berlin Heidelberg. pp. 501-505

12. M.K. Ermakov, S.P. Vartanov. Applying Java bytecode static instrumentation for software dynamic analysis. Trudy ISP RAN / Proc. ISP RAS, vol 27, issue 1, 2015, pp. 25-38 (in Russian). DOI: 10.15514/ISPRAS-2015-27(1)-2.