Verifying android applications using Java PathFinder

Authors:
Open Access
Publisher website
Google Scholar
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.