Compositional Verification for Component-based Systems and Application - Inria - Institut national de recherche en sciences et technologies du numérique Accéder directement au contenu
Article Dans Une Revue IET Software Année : 2010

Compositional Verification for Component-based Systems and Application

Marius Bozga
Saddek Bensalem
Thanh-Hung Nguyen
  • Fonction : Auteur
  • PersonId : 857881
Joseph Sifakis
  • Fonction : Auteur
  • PersonId : 857859

Résumé

We present a compositional method for the verification of component-based systems described in a subset of the BIP language encompassing multi-party interaction without data transfer. The method is based on the use of two kinds of invariants. Component invariants are over-approximations of components' reachability sets. Interaction invariants are global constraints on the states of components involved in interactions. The method has been implemented in the D-Finder tool and has been applied for checking deadlock-freedom. The experimental results on non-trivial examples show that our method allow either to prove deadlock-freedom or to identify very few deadlock configurations that can be analyzed by using state space exploration.

Dates et versions

hal-00568866 , version 1 (23-02-2011)

Identifiants

Citer

Marius Bozga, Saddek Bensalem, Thanh-Hung Nguyen, Joseph Sifakis. Compositional Verification for Component-based Systems and Application. IET Software, 2010, 4 (3), pp.181-193. ⟨10.1049/iet-sen.2009.0011⟩. ⟨hal-00568866⟩
131 Consultations
0 Téléchargements

Altmetric

Partager

Gmail Facebook X LinkedIn More