Running Android applications on JPF

The *.jpf file

Every application verified on JPF requires at least one *.jpf application property file. An example of such a file is given in the listing below. This file defines the target of the application i.e. where JPF should start execution. The JPF property file also contains the name of the input script file and the Checklist definition file for this project.

Example of a *.jpf properties file

#--- dependencies on other JPF projects
@using = jpf-android

#--- target setup
target = com.example.calculator.SimpleActivity

#--- project path is used by jpf-android to find and parse the R.java and layout resources
projectpath=${jpf-android}/../Applications/Calculator

#--- classpath setup (uncomment the first line if building with ant or second line if building with gradle)

classpath+=${jpf-android}/../Applications/Calculator/bin/classes/;${jpf-android}/../Applications/Calculator/libs/EvalEx-1.0.jar;

#classpath+=${jpf-android}/../Applications/Calculator/build/classes/release;${jpf-android}/../Applications/Calculator/libs/EvalEx-1.0.jar;

sourcepath=${jpf-android}/../Applications/Calculator/src;


#--- android setup
android.script=${config_path}/TestCalculator2.es
android.checklist_enabled = false

#--- enable coverage analyzer
listener+=.listener.CoverageAnalyzer
coverage.include = com.example.calculator.*
coverage.show_methods = true
coverage.show_branches = false

#--- search class
search.class = .search.heuristic.BFSHeuristic


#--- reporting
# don't obfuscate things in handlers
vm.halt_on_throw=java.lang.ArithmeticException

The classpath is the location of the .class files of the project. In other words the location JPF will go to lookup classes when it has to load a class. For Android projects these class files are compiled to <project-dir>/bin/classes/ when using ant or <project-dir>/build/classes/release when using gradle.

The sourcepath is the location of the .java files of the project. For Android projects these .java files are in the <project-dir>/src directory.

The android.script is the location and name of the JPF-Android input script for the project. The config-path variable points to the <project-dir>/src directory.

The android.checklist specifies the properties of the checklist framework.
android.checklist.enabled : (true|false) android.checklist.script : path/to/input/script.es android.checklist.active : comma separated list of checklists

The target of the application is the class containing the main method starting the application. Android applications do not have a main method. They are controlled by the Android system invoking callback methods on their components, corresponding to specific life-cycle stages. Each Android application has a launcher or main Activity. JPF-Android uses this Activity as the main entry point of the application. The target in the JPF properties file has to be set to the name of this Activity. When the application is started, JPF loads the target class of the application. A main method is injected into this Activity by JPF-Android.

When the application has finished setting up, it retrieves events from the input script to drive the execution of the application. After the last event in the input script has been processed, the application is shut down

Scripting file (*.es)

Now open the scripting file TestCalculator/src/TestCalculator_NoErr.es:

SECTION default {
  @startIntent.setComponent("com.example.calculator.SimpleActivity")
  startActivity(@startIntent)
}

SECTION com.example.calculator.SimpleActivity {
  $button[0-9].onClick()
  $button<Minus|Mul|Div>.onClick()
  $button[0-9].onClick()
  $buttonEquals.onClick()
}

The script is divided into Sections. Each of these Sections stores th input event of a Window. Most Activities only have one Window, but Activities containing dialogs can have more than one Window as a dialog is also a Window (Discussed in more detail in system docs later).

The "default" section is the section where the script is started. At this point the application has not been launched. The first event that is generated from the script is a external event from the system that asks the application to start the SimpleActivity

When a new event has to be read, the Window Manager checks to see what window/Activity is currently visible. It then requests the next event from that section of the script.

The $ sign indicates that we are referencing a view object defined in the .xml layout files of the Android application.

The script supports non-determinism in the form of collection operators: "[0-2]" and <Plus|Minus>. Please refer to the Scripting section and the papers for more details.

Running

> cd jpf-android/Applications/Calculator
> java -jar ../../../jpf-core/build/RunJPF.jar +info +log src/TestCalculator_Exception.jpf

====================================================== error 1
gov.nasa.jpf.vm.NoUncaughtExceptionsProperty
java.lang.ArithmeticException: Division undefined
  at java.math.BigDecimal.divide(BigDecimal.java:1668)
  at com.udojava.evalex.Expression$4.eval(Expression.java:490)
  at com.udojava.evalex.Expression.eval(Expression.java:852)
  at com.example.calculator.CalculatorActivity.calculate(CalculatorActivity.java:135)
  at com.example.calculator.CalculatorActivity.onClick(CalculatorActivity.java:96)
  at android.view.View.onClick(View.java:463)
  at java.lang.reflect.Method.invoke(gov.nasa.jpf.vm.JPF_java_lang_reflect_Method)
  at android.view.Window.handleViewAction(Window.java:211)
  at android.view.WindowManager.handleViewAction(WindowManager.java:52)
  at android.os.MessageQueue.getNextScriptAction(gov.nasa.jpf.android.JPF_android_os_MessageQueue)
  at android.os.MessageQueue.next(MessageQueue.java:59)
  at android.os.Looper.loop(Looper.java:88)
  at android.app.ActivityThread.main(ActivityThread.java:2199)
  at android.os.ServiceManager.start(ServiceManager.java:73)
  at com.example.calculator.SimpleActivity.main(SimpleActivity.java:0)

====================================================== error input sequence

@startIntent.setComponent("com.example.calculator.SimpleActivity")
startActivity("@startIntent")
$button0.onClick()
$buttonDiv.onClick()
$button0.onClick()
$buttonEquals.onClick()

====================================================== coverage statistics

-------------------------------------------- class coverage ------------------------------------------------
bytecode            line                basic-block         branch              methods             location
------------------------------------------------------------------------------------------------------------
0.68 (311/459)      0.56 (40/71)        0.56 (71/127)       0.00 (0/9)          0.64 (7/11)         com.example.calculator.CalculatorActivity
0.48 (15/31)        0.60 (6/10)         0.62 (8/13)          -                  0.75 (3/4)          com.example.calculator.SimpleActivity

------------------------------------------------------------------------------------------------------------
0.67 (326/490)      0.57 (46/81)        0.56 (79/140)       0.00 (0/9)          0.67 (10/15)        1.00 (2/2)         total

====================================================== results
error #1: gov.nasa.jpf.vm.NoUncaughtExceptionsProperty "java.lang.ArithmeticException: Division undefined ..."

====================================================== statistics
elapsed time:       00:00:06
states:             new=63,visited=0,backtracked=62,end=20
search:             maxDepth=5,constraints=0
choice generators:  thread=2 (signal=0,lock=1,sharedRef=0,threadApi=0,reschedule=1), data=14
heap:               new=25233,released=9797,maxLive=3061,gcCycles=62
instructions:       878232
max memory:         26MB
loaded code:        classes=230,methods=4185

====================================================== search finished: 8/25/14 7:46 AM
            

Using the Eclipse plugin

Another way to run JPF-Android is to install the jpf eclipse plug-in from here.

Right click on a .jpf file. Select the Verify option and the verification process of the system specified in the .jpf file begins

The .jpf file not only indicates the target and classpath, but it also turns on error reporting with trace generation (report.console.property_violation) and configures the source path (sourcepath). Note that multiple source directories are specified using the comma separator. Using eclipse Run Configuration

Select a .jpf file by clicking on it in the Package Explorer Click Run -> Run Configurations -> run jpf-core. It is important the correct .jpf file is selected when the configuration is run.