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

International audienceVerification of component-based systems still suffers from limitations such as state space explosion since a large number of different components may interact in a heterogeneous environment. These limitations entail the need for complementary verification methods such as runtime verification. Runtime verification is a dynamic analysis technique and is prone 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