Compositional Verification for Component-Based Systems and Application

We present a compositional method for the verification of component-based systems described in a subset of the BIP language encompassing multi-party interaction without data transfer. The method is based on the use of two kinds of invariants. Component invariants which are over-approximations of components' reachability sets. Interaction invariants which are constraints on the states of components involved in interactions. Interaction invariants are obtained by computing traps of tate abstractions of the verified system. The method is applied for deadlock verification in the D-Finder tool. D-Finder is 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 analyzed by using state space exploration.

• Type: Conference
• Year: 2008
• Where: ATVA
• Authors: Saddek Bensalem, Marius Bozga, Joseph Sifakis, Thanh-Hung Nguyen
• Keywords: ATVA 2008, Component Invariants, Hardware, Interaction Invariants, Stronger Invariants