-
BUT - Faculty of Information Technology
FIT spiral-of-death

ReplayTracer and BMC

Model Checker JPF

Home Basic Information Download
What is it about?

The model checking of a real system is costly, thus there are some modification or alternations of model checking of features. This website describes the tool RecRev. This tool is about the using of bounded model checking for verification of the bugs in concurrent programs. There is the search strategy for navigation through a state space to a suspicious state (or to its surroundings) and a subsequent bounded model checking initialled from this state. In the first step is record the trace of running program. The second step is replay this trace in some model checker and verify a chosen place in state space only. One of the advantage of these strategy is that the model checking can be started from any of recorded states which precede the suspicious state.

We are concentrate to program written in Java. The model checker for Java program has been chosen Java PathFinder JPF. There is record trace of the running of the program by the IBM ConTest

Main features
  • Replaying program with ConTest instrumentation in JPF - listener
  • Navigation through state space by recorded trace - search strategy
  • Using bounded model checking (BMC) from any control point in recorded trace
  • Possibility of several settings,limits for search strategy and BMC
  • Possibility of extension for next features
Authors
  • Jan Fiedor, ifiedor at fit.vutbr.cz
  • Vendula Hrubá, ihruba at fit.vutbr.cz
  • Bohuslav Křena, krena at fit.vutbr.cz
  • Zdeněk Letko, iletko at fit.vutbr.cz
  • Tomáš Vojnar, vojnar at fit.vutbr.cz
Acknowledgment

This work is partially supported by the European Community under the Information Society Technologies (IST) programme of the 6th FP for RTD - project SHADOWS, contract IST-035157. The authors are solely responsible for the content of this work. It does not represent the opinion of the European Community, and the European Community is not responsible for any use that might be made of data appearing therein.
This work is supported by the Czech Science Foundation (projects GD102/09/H042 and P103/10/0306), the Czech Ministry of Education (projects COST OC10009 and MSM 0021630528), the European Commission (project IC0901), and the Brno University of Technology (project FIT-S-10-1).

Ing.Vendula Hrubá, ihruba at fit.vutbr.cz