Skip to Main content Skip to Navigation
Journal articles

Component-based Verification using Incremental design and Invariants

Abstract : We propose invariant-based techniques for the efficient verification of safety and deadlock-freedom properties of component-based systems. Components and their interactions are described in the BIP language. Global invariants of composite components are obtained by combining local invariants of their constituent components with interaction invariants that take interactions into account.We study new techniques for computing interaction invariants. Some of these techniques are incremental, i.e., interaction invariants of a composite hierarchically structured component are computed by reusing invariants of its constituents. We formalize incremental construction of components in the BIP language as the process of building progressively complex components by adding interactions (synchronization constraints) to atomic components. We provide sufficient conditions ensuring preservation of invariants when new interactions are added. When these conditions are not satisfied, we propose methods for generating new invariants in an incremental manner by reusing existing invariants from the constituents in the incremental construction. The reuse of existing invariants reduces considerably the overall verification effort.The techniques have been implemented in the D-Finder toolset. Among the experiments conducted, we have been capable of verifying safety properties and deadlock-freedom of sub-systems of the functional level of the DALA autonomous robot. This work goes far beyond the capacity of existing monolithic verification tools.
Document type :
Journal articles
Complete list of metadata

Cited literature [67 references]  Display  Hide  Download

https://hal.inria.fr/hal-01087682
Contributor : Uli Fahrenberg <>
Submitted on : Wednesday, November 26, 2014 - 2:56:52 PM
Last modification on : Wednesday, June 16, 2021 - 3:41:36 AM
Long-term archiving on: : Friday, April 14, 2017 - 7:52:13 PM

File

sosym.pdf
Files produced by the author(s)

Identifiers

Citation

Saddek Bensalem, Marius Bozga, Axel Legay, Thanh-Hung Nguyen, Joseph Sifakis, et al.. Component-based Verification using Incremental design and Invariants. Software and Systems Modeling, Springer Verlag, 2014, pp.1-25. ⟨10.1007/s10270-014-0410-8⟩. ⟨hal-01087682⟩

Share

Metrics

Record views

1211

Files downloads

1315