DA-BMC

• Java version 5 or later.
• IBM ConTest tool (not needed for replaying).
• Java PathFinder model checker (revision 285 or 306) (not needed for recording).

The latest version of the DA-BMC tool chain can be downloaded from here and contains:

• Advanced Program Trace Replayer (aptr.jar) for replaying a trace in JPF.
• Contains listeners and search strategies for navigating through a state space in JPF.
• Development Libraries for Java (dev-libs.jar) needed by the Advanced Program Trace Replayer.
• Contains classes used by the Advanced Program Trace Replayer.
• Translation tables (ctm2bt.table and ctm2bt.table) needed by the Advanced Program Trace Replayer.
• Contain information about the types of events which a code instrumented by ConTest may produce.
• Trace Generator (tracegen.jar) for recording a trace in ConTest.
• Contains a listener for recording some of the events monitored by ConTest.
• Thread, synchronisation, memory-access, and control-related events (tracegen-tsac.jar)
• Thread, synchronisation, and memory-access-related events only (tracegen-tsa.jar)
• Thread, synchronisation, and control-related events only (tracegen-tsc.jar)
• Bash script (run-aptr.sh) simplifying the replaying of traces in JPF.
• Configures the replay part of the DA-BMC tool chain.
• Replays a trace of a program in JPF searching for data races.
• Usage: ./run-aptr.sh <trace-file> <entry-class> [-cp <path-to-class-files>] <args>
• If no path to class files is specified, the current working directory will be used.

Below, one can find several simple examples showing how to replay a trace of a program using the DA-BMC tool chain. Each of the examples contains the source code (java files) of the example, the byte code (class files) instrumented by ConTest, which is required for replaying a trace of the program, and a recorded trace leading to an error. Each example also contains a script (replay-<example>.sh) for replaying the trace attached to the example (utilises the run-aptr.sh script). The easiest way to run these examples is to extract them to the same directory where you extracted the DA-BMC tool chain and run the appropriate replay-<example>.sh script. If the RunJPF.jar file is not detected (the script will try to extract the path to this file from the JPF's site.properties, firstly trying to find the JPF's home directory, then the JPF core's home directory and then the path to the RunJPF.jar file), set the RUNJPF variable in the run-aptr.cfg file to an appropriate path.

• Airlines: airlines.tar.gz
• Bank: bank2.tar.gz

This software is provided under the BUT Freeware Licence.

Copyright © 2009-2011, Brno University of Technology. All rights reserved.