Compositional verification for component-based systems and application

The authors present a compositional method for the verification of component-based systems described in a subset of the behaviour-interaction-priority language encompassing multi-party interaction without data transfer. The method is based on the use of two kinds of invariants. Component invariants are over-approximations of components´ reachability sets. Interaction invariants are global constraints on the states of components involved in interactions. The method has been implemented in the D-Finder tool and has been applied for checking deadlock-freedom. The experimental results on non-trivial examples show that this method allows either to prove deadlock-freedom or to identify very few deadlock configurations that can be analysed by using state-space exploration.