Saddek Bensalem, Thanh-Hung Nguyen, Joseph Sifakis, Rongjie Yan
Incremental Component-based Construction and Deadlock Checking (2009)
Incremental Component-based Construction and Deadlock Checking (2009)
TR-2009-12.pdf
TR-2009-12.ps
Keywords: component-based, BIP, connectors, incremental construction, incremental verification, deadlock-freedom
Abstract: We study a methodology for checking incrementally deadlock-freedom of component-based systems. A system is obtained as the composition of atomic components by using interactions. Each interaction expresses strong synchronization (rendezvous) between actions of the components. We improve the heuristic verification method applied by the D-Finder tool to BIP components. The method consists in computing symbolically global invariants for composite components by solving a set of boolean behavioral constraints. The new incremental verification method allows the computation of these global invariants by using a decomposition of the constraints based on the structure of a composite component. We formalize the construction process of a composite component froma set of atomic components. We provide results relating invariants of constituent components used in the construction process, to global invariants. In particular, we show how the boolean behavioral constraints of the composed components are related to those of the product system. Experimental results by using the D-Finder tool for checking deadlock-freedom show significant gains in performance with respect to the global verification technique.
