BeJC

Overview

Download

Running

Publications

Behavior Java Checker

Authors

Overview

BeJC is a tool for checking consistency between component implementation in Java and specification in the language of Threaded Behavior Protocols (TBP) [pdf]. Behavior specification of a component in TBP defines sequences of method calls that the component must handle (i.e., permitted usage of the component) and also sequences of calls that each method is allowed to perform. The component's implementation is consistent with the specification if it responds to all permitted calls on its interfaces in a way allowed by the specification.

Consistency checking involves state space traversal of a Java program composed of the component and automatically generated environment (test harness). BeJC uses the Java PathFinder model checker for this purpose. Detailed description of the checking algorithm and its implementation is in the master thesis of Pavel Jancik [pdf].

Download

Running

The recommended way to run BeJC is to use the run.Checker.{bat/sh} script.
The script has the following parameters:

• Path to the directory with source code of the component
• The configuration file for BeJC.
• Additional model classes for JPF. It is usually safe to use the default value . (when no additional classes are needed)

Example: to check the IpAddressMamanger component (err-spec version) from the package tutorial-0.4.zip, run this command:

  run.Checker.bat src IpAddressManager.cfg .

Input

Example of the configuration file:

component.name=IpAddressManager
component.implclass=ftdemo.IpAddressManagerImpl
env.valuesets=envvaluedb.IpAddrManagerTestValuesDB
env.protocol=./IpAddressManager.tbp
component.provitfs=ITimerCallback-ftdemo.ITimerCallback;IDhcpListenerCallback-ftdemo.IDhcpListenerCallback
component.reqitfs=ITimer-ftdemo.ITimer

Output

• Header contains the processed TBP specification and the JPF header.

  Phase III - Running patched JPF to check specification compilance
  JavaPathfinder v6.0 - (C) RIACS/NASA Ames Research Center
  
  
  ====================================================== system under test
  application: ftdemo/IpAddressManager_main.java
  
  ====================================================== search started: 1.9.11 15:28
  

• Component output contains everything that the component writes to the console. Due to backtracking, it reflects multiple execution paths.
• The last part (result) contains various statistics, where some are related to JPF and other to BeJC, and the checking result.

  Dumping histogram of Number of the TBPStates mapped to JPFState -> Number of occurences
  	1 ->261289
  	2 ->46098
  	3 ->1716
  	4 ->911
  
  
  ====================================================== results
  error #1: org.ow2.dsrg.fm.tbpjava.checker.ProtocolListener "Tested component is not compliant with the protocol"
  
  ====================================================== statistics
  elapsed time:       0:06:38
  states:             new=310090, visited=661459, backtracked=971468, end=45
  search:             maxDepth=105, constraints hit=0
  choice generators:  thread=273941 (signal=0, lock=87641, shared ref=127854), data=88417
  heap:               new=113465, released=117263, max live=1939, gc-cycles=715060
  instructions:       7676240
  max memory:         202MB
  loaded code:        classes=124, methods=1636
  
  ====================================================== search finished: 1.9.11 15:35
  

  The three possible results of checking with BeJC are: "No error detected", "Component not compliant with protocol", "Error during processing".
  • The result "No error detected" means that the component implementation is consistent with the TBP specification.
  • The result "Component not compliant with protocol" means that the implementation of the component violates the TBP specification. In this case the output of BeJC contains three additional parts: trace with the executed code, snapshot of the Java program (call stack of all threads), and counterexample in the TBP specification (events on the component interfaces which lead to the error such that the last one is not permitted by the TBP specification). The error output looks like this:
    

    ====================================================== snapshot #1
    thread index=0,name=main,status=RUNNING,this=java.lang.Thread@0,target=null,priority=5,lockCount=0,suspendCount=0
      call stack:
            at gov.nasa.jpf.jvm.Verify.random(Verify.java:-1)
            at de.itemis.qimpress.showcase.pricing_simulator.be.service.PricingManager_main.runEnvironment(PricingManager_main.java:38)
            at de.itemis.qimpress.showcase.pricing_simulator.be.service.PricingManager_main.main(PricingManager_main.java:101)
    

    Interface calls event trace
    Event type     | Thread| IF type  | Interface name                    | Method name
    ---------------------------------------------------------------------------------
    ...
    call           | 1     | provided | IDhcpListenerCallback             | RequestNewIpAddress
    call           | 1     | required | IIpMacTransientDb                 | GetIpAddress
    return         | 1     | required | IIpMacTransientDb                 | GetIpAddress
    call           | 1     | required | IIpMacTransientDb                 | Add
    return         | 1     | required | IIpMacTransientDb                 | Add
    call           | 1     | required | ITimer                            | SetTimeout
    

  • The result "Error during processing" indicates technical problems such as an invalid configuration, insufficient memory, etc.

Troubleshooting

• Problem: Could not reserve enough space for object heap
  You are trying to give more memory to Java than it is available. If you use the run.Checker.bat script to run BeJC, edit the java_mem variable in the script (the value is in GB). If you use the run.Checker.sh script, edit the ulimit_mem variable in the script.
• Problem: "ERROR - Cannot found java compiler to compile generated files. (Do you have JDK installed?)."
  BeJC is not executed by JDK, but by JRE that does not include a Java compiler.

Related Publications

2009 (1)

Refereed (journals/proceedings)

2006 (1)

Technical Reports

2005 (1)

Refereed (journals/proceedings)