Please use this identifier to cite or link to this item: https://hdl.handle.net/10356/59248
Title: Formal modelling and verification on Android platform
Authors: Lim, Jolene Yu Han
Keywords: DRNTU::Engineering::Computer science and engineering
Issue Date: 2014
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.
URI: http://hdl.handle.net/10356/59248
Rights: Nanyang Technological University
Fulltext Permission: restricted
Fulltext Availability: With Fulltext
Appears in Collections:SCSE Student Reports (FYP/IA/PA/PI)

Files in This Item:
File Description SizeFormat 
AmendedFinalReport.pdf
  Restricted Access
1.57 MBAdobe PDFView/Open

Google ScholarTM

Check

Items in DR-NTU are protected by copyright, with all rights reserved, unless otherwise indicated.