Automated Analysis and Verification Research Group (VeriFIT) Brno University of Technology (BUT)
FIT spiral-of-death

DA-BMC

A Tool Chain Combining Dynamic Analysis and Bounded Model Checking

Home Tool Description Download
Java PathFinder (JPF) model checker

Java PathFinder (JPF) is an explicit-state model checker for Java byte-code, implemented over a specialised Java virtual machine. JPF provides several state space search strategies like depth-first search (DFS) or breadth-first search (BFS) as well as a listener-based mechanism allowing new user-specific strategies to be defined. We exploit this feature in our work to implement a navigation through a state space based on a (partially) recorded suspicious run of a given program.

JPF implements several techniques for state space reduction, including the partial order reduction (POR) which is based on the observation that a large number of possible thread interleavings are irrelevant for the properties being checked in concurrent programs. JPF automatically detects which schedules are relevant when checking a certain property. Moreover, JPF provides a mechanism to influence the mechanism of choosing the relevant schedules. This is important for us because, on one hand, we cannot avoid partial order reduction not to significantly increase the number of explored states, and, on the other hand, the implicit partial order reduction of JPF may interfere with our intention to reconstruct a certain specific run of a given program.

Recording a Trace using the IBM Contest tool

We have implemented the trace recording on top of the infrastructure provided by the IBM Contest tool. Contest provides a heuristic noise injection mechanism, to increase probability of manifestation of concurrency-related errors, and a listener architecture, implemented via a Java byte-code instrumentation, for retrieving various information about the program being monitored. We use the listener architecture to record some information (monitored events) during the execution of the monitored program.

Each monitored event contains information about the source-code location from which it was generated (class and method name, line and instruction number) and the thread which generated it.

Replaying a Trace in JPF and performing bounded model checking (BMC)
Search Strategy for Replaying Traces

ReplayHeuristicSearch is a new search strategy for navigation through a state space of a program in the JPF model checker based on the information contained in a recorded trace. The approach for navigation through a state space has been proposed and published in the article Self-Healing Assurance Based on Bounded Model Checking in EUROCAST 2009.

The ReplayHeuristicSearch simply tries to generate some execution whose underlying trace corresponds with a recorded trace. It is also possible to let the model checker generate more executions with the same trace.

Bounded Model Checking (BMC)

Bounded model checking is performed in the vicinity of the replayed executions, trying to confirm that there is really some error in the program and/or to debug the recorded suspicious behaviour. The verification listeners looking for occurrences of errors may be activated either at the very beginning of replaying of a trace, or they may be activated at the beginning of each application of bounded model checking. The users can adjust the bounded model checking settings (the depth of the bounded model checking as well as the number of backward steps). This approach is not complete, however the full model checking is much more time costly.

For instance, we are using the PreciseRaceDetector listener available in JPF for checking whether a data race is real. But JPF allows to add other user-specific listeners for checking the required features of programs.

Vendula Hrubá (ihruba AT fit.vutbr.cz), Jan Fiedor (ifiedor AT fit.vutbr.cz)