D-Finder: A Tool for Compositional Deadlock Detection and Verification

D-Finder tool implements a compositional method for the verification of component-based systems described in BIP language encompassing multi-party interaction. For deadlock detection, D-Finder applies proof strategies to eliminate potential deadlocks by computing increasingly stronger invariants. 1 Methodology Compositional verification techniques are used to cope with state explosion in concurrent systems. The idea is to aply divide-and-conquer approaches to infer global properties of complex systems from properties of their components. Separate verification of components limits state explosion. Nonetheless, components mutually interact in a system and their behavior and properties are inter-related. This is a major difficulty in designing compositional techniques [1?8]). As explained in [9], compositional rules are in general of the form B1 < 1 >, B2 < 2 >, C(1, 2, ) B1 B2 < > (1) That is, if two components with behaviors B1, B2 meet individually properties 1, 2 re...

• Type: Conference
• Year: 2009
• Where: CAV
• Authors: Saddek Bensalem, Marius Bozga, Thanh-Hung Nguyen, Joseph Sifakis
• Keywords: CAV 2009, Compositional Verification Techniques, Formal Methods, Global Invariants, N-ary Composition Operation