More Web Proxy on the site http://driver.im/

research-article

Verifying android applications using Java PathFinder

Authors:

Heila van der Merwe,

Brink van der Merwe,

Willem VisserAuthors Info & Claims

ACM SIGSOFT Software Engineering Notes, Volume 37, Issue 6

Pages 1 - 5

https://doi.org/10.1145/2382756.2382797

Published: 27 November 2012 Publication History

Abstract

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 development of JPF-ANDROID, an Android application verification tool. JPF-ANDROID is built on Java Pathfinder, a Java model checking engine. JPF-ANDROID provides a simplified model of the Android framework on which an Android application can run. It then allows the user to script input events to drive the application flow. JPF-ANDROID provides a way to detect common property violations such as deadlocks and runtime exceptions in Android applications.

References

[1]

Android documentation. http://developer.android.com/. Accessed: 17 July 2012.

[2]

Java Pathfinder documentation. http://babelfish.arc.nasa.gov/trac/jpf. Accessed: July 2012.

[3]

Android mock, November 2007. http://code.google.com/p/android-mock/. Accessed: 17 July 2012.

[4]

Mockito, November 2007. http://code.google.com/p/mockito/. Accessed: 17 July 2012.

[5]

Robolectric documentation, November 2007. http://pivotal.github.com/robolectric. Accessed: July 2012.

[6]

User scenario testing for android, November 2007. code.google.com/p/robotium/. Accessed: 17 July 2012.

[7]

Testing fundamentals, June 2012. http://developer.android.com/tools/testing/. Accessed: 17 July 2012.

[8]

D. Ehringer. The Dalvik virtual machine architecture. 2010.

[9]

M. Grechanik, Q. Xie, and C. Fu. Creating gui testing tools using accessibility technologies. In International Conference on Software Testing, Verification and Validation Workshops (ICSTW), pages 243--250, April 2009.

Digital Library

[10]

G. Hamilton. Multithreaded toolkits: A failed dream?, October 2004. http://weblogs.java.net/blog/kgh/archive/2004/10/multithreaded_t.html. Accessed: 17 July 2012.

[11]

C. Hu and I. Neamtiu. Automating gui testing for android applications. In Proceedings of the 6th International Workshop on Automation of Software Test, AST '11, pages 77--83, New York, NY, USA, 2011. ACM.

Digital Library

[12]

C. Hu and I. Neamtiu. Automating gui testing for android applications. In Proceedings of the 6th International Workshop on Automation of Software Test, AST '11, pages 77--83, New York, NY, USA, 2011. ACM.

Digital Library

[13]

H. Ji. Mobile software testing based on simulation keyboard. In Q. Luo, editor, Advances in Wireless Networks and Information Systems, volume 72 of Lecture Notes in Electrical Engineering, pages 555--561. Springer Berlin Heidelberg, 2010.

[14]

P. Mehlitz, O. Tkachuk, and M. Ujma. JPF-AWT: Model checking gui applications. In 2011 26th IEEE/ACM International Conference on Automated Software Engineering (ASE), pages 584--587, November 2011.

Digital Library

[15]

E. Pasko. Google android, apache harmony and java packaging, 2007. http://apache-harmony.blogspot.com/2007/11/google-android-apache-harmony-and-java.html. Accessed: July 2012.

[16]

T. Schreiber, J. Somorovsky, and D. Bußmeyer. Android Binder. {seminarthesis}, October 2011.

[17]

J. Six. Application Security for the Android Platform. O'Reilly Media, Inc., December 2011.

[18]

M. Staats. Towards a framework for generating tests to satisfy complex code coverage in Java Pathfinder. In Proc. of NASA Formal Methods Symposium 2009, page 116, 2009.

[19]

K. Yaghmour. Understanding the Android System Server. In AnDevCon, Android conference, 2011.

Cited By

Sun JSu TSun JLi JWang MPu Gd'Amorim M(2024)Property-Based Testing for Validating User Privacy-Related Functionalities in Social Media AppsCompanion Proceedings of the 32nd ACM International Conference on the Foundations of Software Engineering10.1145/3663529.3663863(440-451)Online publication date: 10-Jul-2024
https://dl.acm.org/doi/10.1145/3663529.3663863
Wu SLi JZhou HFang YZhao KWang HQian CLuo XJust RFraser G(2023)CydiOS: A Model-Based Testing Framework for iOS AppsProceedings of the 32nd ACM SIGSOFT International Symposium on Software Testing and Analysis10.1145/3597926.3598033(1-13)Online publication date: 12-Jul-2023
https://dl.acm.org/doi/10.1145/3597926.3598033
Auer MStahlbauer AFraser G(2023)Android Fuzzing: Balancing User-Inputs and Intents2023 IEEE Conference on Software Testing, Verification and Validation (ICST)10.1109/ICST57152.2023.00013(37-48)Online publication date: Apr-2023
https://doi.org/10.1109/ICST57152.2023.00013
Show More Cited By

Index Terms

Verifying android applications using Java PathFinder
1. Software and its engineering
  1. Software creation and management
    1. Software verification and validation
      1. Software defect analysis
        Software testing and debugging

Recommendations

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 ...
Automatic handling of native methods in Java PathFinder
SPIN 2014: Proceedings of the 2014 International SPIN Symposium on Model Checking of Software

Java PathFinder (JPF) is a model checker for Java applications. Despite its maturity, JPF cannot be used to verify any realistic Java application without a nontrivial amount of work done by its user. One of the main limiting factors towards model ...

Comments

Please enable JavaScript to view thecomments powered by Disqus.

Information & Contributors

Information

Published In

cover image ACM SIGSOFT Software Engineering Notes

ACM SIGSOFT Software Engineering Notes Volume 37, Issue 6

November 2012

191 pages

ISSN:0163-5948

DOI:10.1145/2382756

Issue’s Table of Contents

Copyright © 2012 Copyright is held by the owner/author(s).

Permission to make digital or hard copies of part or all of this work for personal or classroom use is granted without fee provided that copies are not made or distributed for profit or commercial advantage and that copies bear this notice and the full citation on the first page. Copyrights for third-party components of this work must be honored. For all other uses, contact the Owner/Author.

Publisher

Association for Computing Machinery

New York, NY, United States

Publication History

Published: 27 November 2012

Published in SIGSOFT Volume 37, Issue 6

Check for updates

Author Tags

Qualifiers

Research-article

Contributors

Other Metrics

View Article Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

57
Total Citations
View Citations
1,211
Total Downloads

Downloads (Last 12 months)12
Downloads (Last 6 weeks)0

Reflects downloads up to 31 Dec 2024

Other Metrics

View Author Metrics

Citations

Cited By

Sun JSu TSun JLi JWang MPu Gd'Amorim M(2024)Property-Based Testing for Validating User Privacy-Related Functionalities in Social Media AppsCompanion Proceedings of the 32nd ACM International Conference on the Foundations of Software Engineering10.1145/3663529.3663863(440-451)Online publication date: 10-Jul-2024
https://dl.acm.org/doi/10.1145/3663529.3663863
Wu SLi JZhou HFang YZhao KWang HQian CLuo XJust RFraser G(2023)CydiOS: A Model-Based Testing Framework for iOS AppsProceedings of the 32nd ACM SIGSOFT International Symposium on Software Testing and Analysis10.1145/3597926.3598033(1-13)Online publication date: 12-Jul-2023
https://dl.acm.org/doi/10.1145/3597926.3598033
Auer MStahlbauer AFraser G(2023)Android Fuzzing: Balancing User-Inputs and Intents2023 IEEE Conference on Software Testing, Verification and Validation (ICST)10.1109/ICST57152.2023.00013(37-48)Online publication date: Apr-2023
https://doi.org/10.1109/ICST57152.2023.00013
Bose PDas DVasan SMariani SGrishchenko IContinella ABianchi AKruegel CVigna G(2023)Columbus: Android App Testing Through Systematic Callback Exploration2023 IEEE/ACM 45th International Conference on Software Engineering (ICSE)10.1109/ICSE48619.2023.00121(1381-1392)Online publication date: May-2023
https://doi.org/10.1109/ICSE48619.2023.00121
Wang T(2023)ConfigDroid: Configuration-aware GUI testing of Android Applications2023 3rd International Conference on Consumer Electronics and Computer Engineering (ICCECE)10.1109/ICCECE58074.2023.10135349(615-619)Online publication date: 6-Jan-2023
https://doi.org/10.1109/ICCECE58074.2023.10135349
Cheng CLin LShi CGuan Y(2023)An Anti-Fuzzing Approach for Android AppsAdvances in Digital Forensics XIX10.1007/978-3-031-42991-0_3(37-53)Online publication date: 19-Oct-2023
https://doi.org/10.1007/978-3-031-42991-0_3
Su TFan LChen SLiu YXu LPu GSu Z(2022)Why My App Crashes? Understanding and Benchmarking Framework-Specific Exceptions of Android AppsIEEE Transactions on Software Engineering10.1109/TSE.2020.301343848:4(1115-1137)Online publication date: 1-Apr-2022
https://doi.org/10.1109/TSE.2020.3013438
Liu AGuo CDong NWang YXu J(2022)DALT: Deep Activity Launching Test via Intent-Constraint Extraction2022 IEEE 33rd International Symposium on Software Reliability Engineering (ISSRE)10.1109/ISSRE55969.2022.00053(482-493)Online publication date: Oct-2022
https://doi.org/10.1109/ISSRE55969.2022.00053
Silva BStevens CMansoor NSrisa-An WYu TBagheri H(2022)SAINTDroid: Scalable, Automated Incompatibility Detection for Android2022 52nd Annual IEEE/IFIP International Conference on Dependable Systems and Networks (DSN)10.1109/DSN53405.2022.00062(567-579)Online publication date: Jun-2022
https://doi.org/10.1109/DSN53405.2022.00062
Su TYan YWang JSun JXiong YPu GWang KSu Z(2021)Fully automated functional fuzzing of Android apps for detecting non-crashing logic bugsProceedings of the ACM on Programming Languages10.1145/34855335:OOPSLA(1-31)Online publication date: 15-Oct-2021
https://dl.acm.org/doi/10.1145/3485533
Show More Cited By

View Options

Login options

Check if you have access through your login credentials or your institution to get full access on this article.

Full Access

Get this Publication

View options

PDF

View or Download as a PDF file.

eReader

View online with eReader.

Media

Figures

Other

Tables

View Issue’s Table of Contents