Formal modelling and verification on Android platform

Abstract

Today’s mobile applications deliver complex functionalities on the Google’s Android platform. This underscores the growing need for automated testing techniques, so as to ensure quality of the mobile applications. By conducting an exhaustive exploration of the state system of an application, automated testing tools such as Java PathFinder, possess the ability to check and report traces of events leading to the violation of the specifications. However, for Android applications to leverage on the benefits of this model checking tool, the application must first be compiled into Java byte codes.

To execute an application on the Java Virtual Machine, the Android libraries first have to be modelled through the creation of stubs and mock classes, before the application’s driver file could be generated. After the modification process, the Android application is ready to be executed on the Java Virtual Machine platform. The number of modelled Android libraries will increase after each round of application testing, thus developing the mock up Android framework progressively.

The details of the project’s development and its implementation are will be discussed in the next section. Last but not least, a total of 20 Android applications were tested using the Java PathFinder in the later part of the project. Apart from detecting the application’s property violation, Java PathFinder is able to verify if the application divulge device data.

As the concept of implementing Android application on Java PathFinder is relatively new, the amount of resources available is limited. This report is useful to researchers who are interested to learn more about the adopted approach and implementation details. This report will also demonstrate how Java PathFinder could be used to discover security flaws within an application.