Abstract
In this paper, we propose to base the verification of a GUI application on a reference model used in black-box testing. The reference model is a formal model for the behavior of the GUI application. It is derived by dynamic analysis (hence “black-box”). Thus, it can be used to account for the graphical interface even when the GUI toolkit is not amenable to formal analysis or its source code is not available. We have implemented our approach; a preliminary case study indicates its feasibility in principle.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
Similar content being viewed by others
References
Arlt, S., Podelski, A., Bertolini, C., Schaef, M., Banerjee, I., Memon, A.M.: Lightweight Static Analysis for GUI Testing. In: ISSRE, pp. 301–310 (2012)
Arlt, S., Podelski, A., Wehrle, M.: Reducing GUI Test Suites via Program Slicing. In: ISSTA, pp. 270–281 (2014)
Arlt, S., Schäf, M.: Joogie: Infeasible Code Detection for Java. In: Madhusudan, P., Seshia, S.A. (eds.) CAV 2012. LNCS, vol. 7358, pp. 767–773. Springer, Heidelberg (2012)
Barnett, M., Chang, B.-Y.E., DeLine, R., Jacobs, B., M. Leino, K.R.: Boogie: A Modular Reusable Verifier for Object-Oriented Programs. In: de Boer, F.S., Bonsangue, M.M., Graf, S., de Roever, W.-P. (eds.) FMCO 2005. LNCS, vol. 4111, pp. 364–387. Springer, Heidelberg (2006)
Belli, F.: Finite-State Testing and Analysis of Graphical User Interfaces. In: ISSRE, pp. 34–43 (2001)
Berstel, J., Crespi-Reghizzi, S., Roussel, G., Pietro, P.S.: A Scalable Formal Method for Design and Automatic Checking of User Interfaces. In: ICSE, pp. 453–462 (2001)
Clarke, E.M., Grumberg, O., Long, D.E.: Model Checking and Abstraction. In: POPL, pp. 342–354 (1992)
Cobleigh, J.M., Giannakopoulou, D., Păsăreanu, C.S.: Learning Assumptions for Compositional Verification. In: Garavel, H., Hatcliff, J. (eds.) TACAS 2003. LNCS, vol. 2619, pp. 331–346. Springer, Heidelberg (2003)
Dijkstra, E.W.: Notes on Structured Programming. Circulated privately (April 1970)
Dwyer, M.B., Carr, V., Hines, L.: Model Checking Graphical User Interfaces Using Abstractions. In: ESEC / SIGSOFT FSE, pp. 244–261 (1997)
Dwyer, M.B., Tkachuk, O., Visser, W.: Analyzing Interaction Orderings with Model Checking. In: ASE, pp. 154–163 (2004)
Feo-Arenis, S.: Evaluation of a Data Structure Invariant Generation Technique. Master’s thesis, University of Freiburg (March 2010)
Ganov, S., Killmar, C., Khurshid, S., Perry, D.E.: Event Listener Analysis and Symbolic Execution for Testing GUI Applications. In: Breitman, K., Cavalcanti, A. (eds.) ICFEM 2009. LNCS, vol. 5885, pp. 69–87. Springer, Heidelberg (2009)
Gross, F., Fraser, G., Zeller, A.: Search-based system testing: high coverage, no false alarms. In: ISSTA, pp. 67–77 (2012)
Heizmann, M., Christ, J., Dietsch, D., Ermis, E., Hoenicke, J., Lindenmann, M., Nutz, A., Schilling, C., Podelski, A.: Ultimate Automizer with SMTInterpol. In: Piterman, N., Smolka, S.A. (eds.) TACAS 2013 (ETAPS 2013). LNCS, vol. 7795, pp. 641–643. Springer, Heidelberg (2013)
Huang, S., Cohen, M.B., Memon, A.M.: Repairing GUI Test Suites Using a Genetic Algorithm. In: ICST, Paris, France (April 2010)
Lindholm, T., Yellin, F.: Java Virtual Machine Specification, 2nd edn. Addison-Wesley Longman Publishing Co., Inc., Boston (1999)
Mariani, L., Pezzè, M., Riganelli, O., Santoro, M.: AutoBlackTest: Automatic Black-Box Testing of Interactive Applications. In: ICST, pp. 81–90 (2012)
McMaster, S., Memon, A.M.: Call-Stack Coverage for GUI Test-Suite Reduction. IEEE Trans. Softw. Eng. (2008)
Memon, A.M.: An event-flow model of GUI-based applications for testing. Softw. Test., Verif. Reliab. 17(3), 137–157 (2007)
Memon, A.M., Banerjee, I., Nagarajan, A.: GUI Ripping: Reverse Engineering of Graphical User Interfaces for Testing. In: WCRE, pp. 260–269 (2003)
Memon, A.M., Pollack, M.E., Soffa, M.L.: Using a Goal-Driven Approach to Generate Test Cases for GUIs. In: ICSE, pp. 257–266 (1999)
Memon, A.M., Pollack, M.E., Soffa, M.L.: Hierarchical GUI Test Case Generation Using Automated Planning. IEEE Trans. Software Eng. 27(2), 144–155 (2001)
Paiva, A.C.R., Faria, J.C.P., Mendes, P.M.C.: Reverse Engineered Formal Models for GUI Testing. In: Leue, S., Merino, P. (eds.) FMICS 2007. LNCS, vol. 4916, pp. 218–233. Springer, Heidelberg (2008)
Raffelt, H., Merten, M., Steffen, B., Margaria, T.: Dynamic testing via automata learning. STTT 11(4), 307–324 (2009)
White, L.J., Almezen, H.: Generating Test Cases for GUI Responsibilities Using Complete Interaction Sequences. In: ISSRE, pp. 110–123 (2000)
Windmüller, S., Neubauer, J., Steffen, B., Howar, F., Bauer, O.: Active continuous quality control. In: CBSE, pp. 111–120 (2013)
Yuan, X., Cohen, M.B., Memon, A.M.: Covering array sampling of input event sequences for automated gui testing. In: ASE, pp. 405–408 (2007)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2014 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Arlt, S., Ermis, E., Feo-Arenis, S., Podelski, A. (2014). Verification of GUI Applications: A Black-Box Approach. In: Margaria, T., Steffen, B. (eds) Leveraging Applications of Formal Methods, Verification and Validation. Technologies for Mastering Change. ISoLA 2014. Lecture Notes in Computer Science, vol 8802. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-662-45234-9_17
Download citation
DOI: https://doi.org/10.1007/978-3-662-45234-9_17
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-662-45233-2
Online ISBN: 978-3-662-45234-9
eBook Packages: Computer ScienceComputer Science (R0)