A Compositional Deadlock Detection and Verification Tool for BIP Models


More details about the compositional deadlock detection and verification method implemented in the D-Finder tool can be found here.

 How To Install and Run D-Finder

Requirements :

  • Linux or Mac OS X.
  • Java 1.6.

The installation of D-Finder requires the following steps :

  • First dowload the D-Finder tool-set
  • Extract the package.
  • Follow the instructions in the INSTALL file to install and configure the third party tools Yices, Omega, and JavaBDD
  • Build your BIP model (here is an example of Dining Philosopher in BIP). More information about BIP modeling framework can be found here.
  • Go to the DFinder directory and run the D-Finder tool to verify your model by the following command :
    • For global methods : ./dfinder -c dfinder.config -f [path-to-model.bip] --method=[pm/linear]
    • For incremental methods : ./dfinder -c dfinder.config -f [path-to-model.bip] --incr_file [incr-file] --method=[pm]
      where :
    • pm : symbolic method based on positive mapping
    • linear : computes linear invariants that might be stronger but is not efficient for large-scale/complex systems.
    • [incr-file] : file that defines set of increments

News : a GUI for D-Finder has been available (for both Linux and Mac OS X). In DFinder directory, run the following script : ./dfinder-gui

 Running Examples

Dining Philosopher

in Terminal, go to D-Finder folder run the global methods by the following command :

./dfinder -c dfinder.config -f examples/philo20.bip --method=pm/fp/linear

or run the incremental methods by the following command :

./dfinder -c dfinder.config -f examples/philo20.bip -incr_file examples/philo20.incr --method=pm/fp

Contact | Plan du site | Site réalisé avec SPIP 2.1.26 + AHUNTSIC [CC License]

Visiteurs connectés : 22 ; visites : 526423