FORTE 2013: P.C Attie, S. Bensalem, M. Bozga, M. Jaber, J. Sifakis, and F. Zaraket
We present a sound but incomplete criterion for checking deadlock-freedom of large systems expressed in BIP: a component-based framework for the construction of complex distributed systems. Since deciding deadlock-freedom for finite-state concurrent systems is PSPACE-complete, our criterion gives up completeness in return for tractability of evaluation. Our criterion can be evaluated by model-checking subsystems of the overall large system. The size of these subsystems depends only on the local topology of direct interaction between components, and not on the number of components in the overall system. We present two experiments, in which our method compares favorably with existing approaches. For example, in verifying deadlock freedom of dining philosophers, our method shows linear increase in computation time with the number of philosophers, whereas other methods (even those that use abstraction) show super-linear increase, due to state-explosion.
LDFC-BIP is a tool for checking deadlock-freedom of large systems expressed in BIP. BIP is a component-based framework supporting rigorous design. It is developed at Verimag Laboratory. For more information about BIP, visit here. Download BIP Compiler and Runtime
LDFC-BIP takes as input a BIP file and checks for local and global deadlock-freedom.
The lastest version of LDFC-BIP is distributed as a ZIPed JAR file, with documentation and examples, running under Java 1.6.
- UNZIP the distribution
- To execute simply run:
java -jar LDFCBIP.jar example/dining.bip [--debug]
--debug: Prints useful information at each iteration of the algorithm.
Example: selected interaction, depth length, etc.
This information could be useful in case when the LDFC condition fails.
Note that, in the current version, we abstract away from issues of variables and data transfer since we are only interested in enablement of ports.