Heila van der Merwe
Willem Visser
Abstract
JPF-Android is a model checking tool for Android applications allowing them to be verified outside of an emulator on Java PathFinder (JPF). The Android applications are executed on a model of the Android software stack and their execution driven by simulating user and system input events. This paper follows from our previous work describing the design decisions and implementation of JPF-Android. Here we discuss the syntax and implementation of the scripting environment which is used to drive the execution of the An- droid application under analysis. It also focuses on a further extension to the tool used to automatically monitor the run- time behavior of Android applications.
- D. Amalfitano, A. R. Fasolino, and P. Tramontana. A GUI Crawling-Based Technique for Android Mobile Application Testing. In 2011 IEEE Fourth International Conference on Software Testing, Verification and Validation Workshops, pages 252--261. IEEE, Mar. 2011. Google Scholar
Digital Library
- F. Chen and G. Roşu. Towards Monitoring-Oriented Programming. Electronic Notes in Theoretical Computer Science, 89(2):108--127, Oct. 2003.Google ScholarCross Ref
- K. Havelund and G. Roşu. Monitoring Java Programs with Java PathExplorer. Electronic Notes in Theoretical Computer Science, 55(2):200--217, Oct. 2001.Google ScholarCross Ref
- K. Havelund and G. Roşu. Efficient monitoring of safety properties. International Journal on Software Tools for Technology Transfer, 6(2):158--173, Nov. 2003. Google ScholarDigital Library
- C. S. Jensen, M. R. Prasad, and A. Møller. Automated Testing with Targeted Event Sequence Generation. In Proc. 22nd International Symposium on Software Testing and Analysis (ISSTA), Lugano, Switzerland, July 2013. Google ScholarDigital Library
- M. Kim, S. Kannan, I. Lee, O. Sokolsky, and M. Viswanathan. Java-MaC: a Run-time Assurance Tool for Java Programs. Electronic Notes in Theoretical Computer Science, 55(2):218--235, Oct. 2001.Google ScholarCross Ref
- A. Machiry, R. Tahiliani, and M. Naik. Dynodroid: An Input Generation System for Android Apps. ACM SIGSOFT Software Engineering Notes, Aug. 2013. Google ScholarDigital Library
- N. Mirzaei, S. Malek, C. S. Pasareanu, N. Esfahani, and R. Mahmood. Testing android apps through symbolic execution. ACM SIGSOFT Software Engineering Notes, 37(6):1, Nov. 2012. Google ScholarDigital Library
- B. Sadeh and S. Gopalakrishnan. A Study on the Evaluation of Unit Testing for Android Systems. International Journal of New Computer Architectures and their Applications (IJNCAA), 4(1):926--941, 2011.Google Scholar
- H. van der Merwe, B. van der Merwe, and W. Visser. Verifying Android applications using Java PathFinder. ACM SIGSOFT Software Engineering Notes, 37(6):1, Nov. 2012. Google ScholarDigital Library
- W. Yang, M. R. Prasad, and T. Xie. A Grey-Box Approach for Automated GUI-Model Generation of Mobile Applications. In Fundamental Approaches to Software Engineering, volume 7793 of Lecture Notes in Computer Science, pages 250--265. Springer Berlin Heidelberg, 2013. Google Scholar
Index Terms
- Execution and property specifications for JPF-android
Recommendations
Verifying android applications using Java PathFinder
Mobile application testing is a specialised and complex field. Due to mobile applications' event driven design and mobile runtime environment, there currently exist only a small number of tools to verify these applications. This paper describes the ...
Testing android apps through symbolic execution
There is a growing need for automated testing techniques aimed at Android apps. A critical challenge is the systematic generation of test cases. One method of systematically generating test cases for Java programs is symbolic execution. But applying ...
Java Pathfinder on Android Devices
Because Android apps are written in Java and executed on a virtual machine (VM), there is an opportunity to employ Java Pathfinder (JPF) for their verification. There already exist two JPF extensions, jpf-android and jpf-pathdroid. The former executes ...
Comments