Runtime verification of component-based systems in the BIP framework with formally-proved sound and complete instrumentation

Abstract : Verification of component-based systems still suffers from limitations such as state space explosion since a large number of different components may interact in an heterogeneous environment. These limitations entail the need for complementary verification methods such as runtime verification based on dynamic analysis and apt to scalability. In this paper, we integrate runtime verification into the BIP (Behavior, Interaction and Priority) framework. BIP is a powerful and expressive component-based framework for the formal construction of heterogeneous systems. Our method augments BIP systems with monitors to check specifications at runtime. This method has been implemented in RV-BIP, a prototype tool that we used to validate the whole approach on a robotic application.
Type de document :
Article dans une revue
Software and Systems Modeling, Springer Verlag, 2015, 14 (1), pp.38. 〈10.1007/s10270-013-0323-y〉
Liste complète des métadonnées

https://hal.inria.fr/hal-01248420
Contributeur : Yliès Falcone <>
Soumis le : samedi 26 décembre 2015 - 11:53:46
Dernière modification le : jeudi 11 janvier 2018 - 06:27:21

Fichier

Sosym-author-version_Falcone-e...
Fichiers produits par l'(les) auteur(s)

Identifiants

Collections

Citation

Yliès Falcone, Mohamad Jaber, Thanh-Hung Nguyen, Marius Bozga, Saddek Bensalem. Runtime verification of component-based systems in the BIP framework with formally-proved sound and complete instrumentation. Software and Systems Modeling, Springer Verlag, 2015, 14 (1), pp.38. 〈10.1007/s10270-013-0323-y〉. 〈hal-01248420〉

Partager

Métriques

Consultations de la notice

379

Téléchargements de fichiers

129