Incremental Component-based Construction and Verification using Invariants

A new method for incremental computation of invariants is proposed, for checking incrementally safety properties of component-based systems described as the composition of interacting components. It improves the method applied by the D-Finder tool based on the computation of global invariants of composite components as solutions of a set of boolean behavioral constraints. These are induced by interactions on transition relations of the composed components. The new method uses a formalization of the incremental construction process of a composite component from a set of atomic components. Following the construction process, it decomposes the computation of global invariants of composite components into the computation of invariants of their constituent components. This is achieved by application of results relating boolean behavioral constraints of constituent components to global boolean behavioral constraints. The new method has been implemented in the D-Finder tool. Experimental results show significant gains in performance by applying the incremental computation of invariants in deadlock checking, with respect to the global verification method.