Concurrency-preserving and sound monitoring of multi-threaded component-based systems: theory, algorithms, implementation, and evaluation

Hosein Nazarpour (1) , Yliès Falcone (2, 3) , Saddek Bensalem (1) , Marius Bozga (1)

1 VERIMAG - IMAG - VERIMAG
2 LIG - Laboratoire d'Informatique de Grenoble
3 CORSE - Compiler Optimization and Run-time Systems

This paper addresses the monitoring of logic-independent linear-time user-provided properties in multi-threaded component-based systems. We consider intrinsically independent components that can be executed concurrently with a centralized coordination for multiparty interactions. In this context, the problem that arises is that a global state of the system is not available to the monitor. A naive solution to this problem would be to plug in a monitor which would force the system to synchronize in order to obtain the sequence of global states at runtime. Such a solution would defeat the whole purpose of having concurrent components. Instead, we reconstruct on-the-fly the global states by accumulating the partial states traversed by the system at runtime. We define transformations of components that preserve their semantics and con-currency and, at the same time, allow to monitor global-state properties. Moreover, we present RVMT-BIP, a prototype tool implementing the transformations for monitoring multi-threaded systems described in the BIP (Behavior, Interaction, Priority) framework, an expressive framework for the formal construction of heterogeneous systems. Our experiments on several multi-threaded BIP systems show that RVMT-BIP induces a cheap runtime overhead.

Domaines: Génie logiciel [cs.SE]; Systèmes embarqués

Hosein Nazarpour, Yliès Falcone, Saddek Bensalem, Marius Bozga. Concurrency-preserving and sound monitoring of multi-threaded component-based systems: theory, algorithms, implementation, and evaluation. Formal Aspects of Computing, 2017, 29 (6), pp.951 - 986. ⟨10.1007/s00165-017-0422-6⟩. ⟨hal-01653883⟩