Saddek Bensalem, Marius Bozga, Thanh-Hung Nguyen and Joseph Sifakis
Compositional Deadlock-Detection and Verification for Component-based Systems (2008)
Compositional Deadlock-Detection and Verification for Component-based Systems (2008)
TR-2008-5.pdf
Keywords: deadlock-detection, compositional methods, invariant generation, abstraction
Abstract: We present a heuristic method for compositional deadlock detection and verification of component-based systems described in a subset of the BIP language encompassing multi-party rendezvous without data transfer. The method consists in using automatically generated invariants to prove non-satisfiability of the predicate characterizing global deadlocks.Two kinds of invariants are generated. Component invariants which are over-approximations of components' reachability sets. Interaction invariants which are constraints on the states of the components involved in interactions. Interaction invariants are obtained by computing traps and locks of finite state abstractions of the verified system. The method is supported by D-Finder, an interactive tool that takes as input BIP programs and applies proof strategies to eliminate potential deadlocks by computing increasingly stronger invariants. The experimental results on non-trivial examples allow either to prove deadlock-freedom or to identify very few deadlock configurations that can be analyzing by using state space exploration.
