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.
Type de document :
Article dans une revue
Software and Systems Modeling, Springer Verlag, 2014, pp.1-25. 〈10.1007/s10270-014-0410-8〉
Liste complète des métadonnées

Littérature citée [67 références]  Voir  Masquer  Télécharger

https://hal.inria.fr/hal-01087682
Contributeur : Uli Fahrenberg <>
Soumis le : mercredi 26 novembre 2014 - 14:56:52
Dernière modification le : mercredi 16 mai 2018 - 11:24:07
Document(s) archivé(s) le : vendredi 14 avril 2017 - 19:52:13

Fichier

sosym.pdf
Fichiers produits par l'(les) auteur(s)

Identifiants

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〉

Partager

Métriques

Consultations de la notice

710

Téléchargements de fichiers

255