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

Yliès Falcone 1, * Mohamad Jaber 2 Thanh-Hung Nguyen 3 Marius Bozga 4 Saddek Bensalem 4
* Auteur correspondant
1 CORSE - Compiler Optimization and Run-time Systems
Inria Grenoble - Rhône-Alpes, LIG - Laboratoire d'Informatique de Grenoble
2 American University of Beirut [Beyrouth]
3 USTH - University of sciences and technologies of hanoi
4 VERIMAG - IMAG - VERIMAG
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 octobre 2018 - 08:48:05

Fichier

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

Identifiants

Collections

IMAG | LIG | INRIA | UGA | LIG_SRCPR | LIG-SRCPR-CORSE | VERIMAG

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〉

Exporter

BibTeX TEI DC DCterms EndNote

Partager

Métriques

Consultations de la notice

437

Téléchargements de fichiers

160

Contact


archive-ouverte@inria.fr