Overview

JPF-Android logo

JPF-Android is an Android application verification tool designed to assist developers in creating robust and error free Android applications.

It is created as an extension to Java PathFinder (JPF), a Java application model checker and analysis engine.

Model checking is an effective approach for verifying the correctness of an application with non-deterministic behavior. Android application execution is influenced by non-deterministic behavior such as the different ways its threads can be interleaved, alternative input sequences and different system states during execution.

JPF-Android does not focus on testing the actual rendering of the application's GUI, it focuses on detecting errors in the logic of the application which results in unexpected and unwanted behavior of the system.

Android applications are executed on a model of the Android software stack and their execution driven by simulating user and system input events on the application. By modeling the Android environment, the tool has full control over the execution of the application and over the state of the Android system. In this respect, many of the other testing tools are limited by the Android software platform since it only allows certain properties of the system state to be changed programmability.

Please Note:

JPF-Android is an ongoing project, i.e. it does not support all Android projects. Look at the What is supported section for supported Android functionality.

Publications

  1. Heila Botha, Brink van der Merwe, Willem Visser, and Oksana Tkachuk.
    Addressing Challenges In Obtaining High Coverage When Model Checking Android Applications.
    In Proceedings of the 2017 International Symposium on Model Checking of Software (SPIN'17), pp. 31-40, July 2017.

  2. Guangdong Bai, Quanqi Ye, Yongzheng Wu, Heila van der Merwe, Jun Sun, Yang Liu, Jin Song Dong, Willem Visser.
    Towards Model Checking Android Applications.
    IEEE Transactions on Software Engineering. 2017. (To appear)

  3. Heila Botha, Brink van der Merwe, Willem Visser, and Oksana Tkachuk.
    StateComparator: Detecting Unbounded Variables Using JPF.
    SIGSOFT Software Engineering Notes 41(6), pp. 1-5, January 2017.

  4. Heila van der Merwe, Oksana Tkachuk, Sean Nel, Brink van der Merwe, and Willem Visser.
    Environment Modeling Using Runtime Values for JPF-Android.
    SIGSOFT Software Engineering Notes 40(6), pp. 1-5, November 2015.

  5. Heila van der Merwe.
    Verification of Android Applications.
    In Proceedings of the 37th International Conference on Software Engineering IEEE Press, Piscataway, NJ, USA, pp. 931-934, 2015.

  6. Heila van der Merwe, Oksana Tkachuk, Brink van der Merwe, and Willem Visser.
    Generation of Library Models for Verification of Android Applications.
    SIGSOFT Software Engineering Notes 40(1), pp. 1-5, February 2015

  7. Heila van der Merwe, Brink van der Merwe, and Willem Visser.
    Execution and property specifications for JPF-android.
    SIGSOFT Software Engineering Notes 39(1), pp. 1-5, February 2014.

  8. Heila van der Merwe, Brink van der Merwe, and Willem Visser.
    Verifying Android Applications using Java PathFinder.
    SIGSOFT Software Engineering Notes 37(6), pp. 1-5, November 2012.