Hosein Nazarpour

Yliès Falcone

Saddek Bensalem

Marius Bozga

Jacques Combaz

Monitoring Multi-Threaded Component-Based Systems

published or not. The documents may come   L'archive ouverte pluridisciplinaire

Introduction

Component-based design is the process leading from given requirements and a set of predefined components to a system meeting the requirements. Building systems from components is essential in any engineering discipline. Components are abstract building blocks encapsulating behaviour. They can be composed in order to build composite components. Their composition should be rigorously defined so that it is possible to infer the behaviour of composite components from the behaviour of their constituents as well as global properties from the properties of individual components.

The problem of building component-based systems (CBSs) can be defined as follows. Given a set of components {B 1 , . . . , B n } and a property of their product state space ϕ, find multiparty interactions γ (i.e., "glue" code) s.t. the coordinated behaviour γ(B 1 , . . . , B n ) meets the property ϕ. It is however generally not possible to ensure or verify the desired property ϕ using static verification techniques, either because of the state-explosion problem or because ϕ can only be decided with runtime information. In this paper, we are interested in complementary verification techniques for CBSs such as runtime verification. In [START_REF] Falcone | Runtime verification of component-based systems in the BIP framework with formally-proved sound and complete instrumentation[END_REF], we introduce runtime verification of sequential CBSs against properties referring to the global states of the system, which, in particular, implies that properties can not be "projected" and checked on individual components. From an input composite system γ (B 1 , . . . , B n ) and a linear-time regular property, a component monitor M and a new set of interactions γ are synthesized to build a new composite system γ (B 1 , . . . , B n , M ) where the property is checked at runtime.

The underlying model of CBSs relies on multiparty interactions which consist of actions that are jointly executed by certain components, either sequentially or concurrently. In the sequential setting, components are coordinated by a single centralized controller and joint actions are atomic. Components notify the controller of their current states. Then, the controller computes the possible interactions, selects one, and then sequentially executes the actions of each component involved in the interaction. When components finish their executions, they notify the controller of their new states, and the aforementioned steps are repeated. For performance reasons, it is desirable to parallelize the execution of components. In the multi-threaded setting, each component executes on a thread and a controller is in charge of coordination. Parallelizing the execution of γ (B 1 , . . . , B n ) yields a bisimilar [START_REF] Milner | Communication and concurrency[END_REF] component ( [START_REF] Basu | Distributed semantics and implementation for systems with interaction and priority[END_REF]) where each synchronized action a occurring on B i is broken down into β i and a where β i represents an internal computation of B i and a is a synchronization action. Between β i and a , a new busy location is added. Consequently, the components can perform their interaction independently after synchronization, and the joint actions become non atomic. After starting an interaction, and before this interaction completes (meaning that certain components are still performing internal computations), the controller can start another interaction between ready components.

The problem that arises in the multi-threaded setting is that a global steady state of the system (where all components are ready to perform an interaction) may never exist at runtime. Note that we do not target distributed but multi-threaded systems in which components execute with a centralized controller, there is a global clock and communication is instantaneous and atomic. We define a method to monitor CBSs against linear-time properties referring to global states. Our method preserves the concurrency and semantics of the monitored system. It transforms the system so that global states can be reconstructed by accumulating partial states at runtime. The execution trace of a multi-threaded CBS is a sequence of partial states. For an execution trace of a multithreaded CBS, we define the notion of witness trace, which is intuitively the unique trace of global states corresponding to the trace of the multi-threaded CBS if this CBS was executed on a single thread. For this purpose, we define transformations allowing to add a new component building the witness trace.

We prove that the transformed and initial systems are bisimilar: the obtained reconstructed sequence of global states from a parallel execution is as the sequence of global states obtained when the multi-threaded CBS is executed with a single thread. We introduce RVMT-BIP, a tool integrated in the BIP tool suite.1 BIP (Behavior, Interaction, Priority) framework is a powerful and expressive component framework for the formal construction of heterogeneous systems. RVMT-BIP takes as input a BIP CBS and a monitor description which expresses a property ϕ, and outputs a new BIP system whose behavior is monitored against ϕ while running concurrently.

Figure 1 overviews our approach. Recall that according to [START_REF] Basu | Distributed semantics and implementation for systems with interaction and priority[END_REF]

Refers to

This paper's contribution Verdicts Fig. 1: Approach overview runs faster than S g because of its parallelism. Thus, if a trace of S g , i.e., σ g , satisfies ϕ, then the corresponding trace of S p , i.e., σ p , satisfies ϕ as well. Naive solutions to monitor S p would be i) to monitor S g with the technique in [START_REF] Falcone | Runtime verification of component-based systems in the BIP framework with formally-proved sound and complete instrumentation[END_REF] and run S p , which ends up with delays in detecting verdicts or ii) to plug the monitor proposed in [START_REF] Falcone | Runtime verification of component-based systems in the BIP framework with formally-proved sound and complete instrumentation[END_REF] in S p , which forces the components to synchronize for the monitor to take a snapshot of the global state of the system. Such approaches would completely defeat the purpose of using multi-threaded models. Instead, we propose a transformation technique to build another system S pg out of S p such that i) S pg and S p are bisimilar (hence S g and S pg are bisimilar), ii) S pg is as concurrent as S p and preserves the performance gained from multi-threaded execution and iii) S pg produces a witness trace, that is the trace that allows to check the property ϕ. Our method does not introduce any delay in the detection of verdicts since it always reconstructs the maximal (information-wise) prefix of the witness trace (Theorem 1). Moreover, we show that our method is correct in that it always produces the correct witness trace (Theorem 2). An extended version of this paper with more detail and proofs is available as [START_REF] Nazarpour | Monitoring multi-threaded component-based systems[END_REF]. Running example. We use a task system, called Task, to illustrate our approach throughout the paper. The system consists of a task generator (Generator) along with 3 task executors (Workers) that can run in parallel. Each newly generated task is handled whenever two cooperating workers are available. A desirable property of system Task is the homogeneous distribution of the tasks among the workers.

Preliminaries and notations.

For two domains of elements E and F , we note

[E → F ] the set of functions from E to F . For two functions v ∈ [X → Y ] and v ∈ [X → Y ], the substitution function noted v/v , where v/v ∈ [X ∪X → Y ∪Y ], is defined as v/v (x) = v (x) if x ∈ X , and v(x) otherwise. Given a set of elements E, e 1 • e 2 • • • e n is
a sequence or a list of length n over E, where ∀i ∈ [1, n] : e i ∈ E. Sequences of assignments are delimited by square brackets for clarity. The empty sequence is noted or [ ], depending on the context. The set of (finite) sequences over E is noted E * . E + is defined as E * \ { }. The length of a sequence s is noted length(s). We define s(i) as the i th element of s and s(i • • • j) as the factor of s from the i th to the j th element. We also note pref(s), the set of prefixes of s s.

t. pref(s) = {s(1 • • • k) | k ≤ length(s)}.
Operator pref is naturally extended to sets of sequences. Function max (resp. min ) returns the maximal (resp. minimal) sequence w.r.t. prefix ordering of a set of sequences. We define function last :

E + → E s.t. last(e 1 • e 2 • • • e n ) = e n .
For a sequence e = e 1 • e 2 • • • e n over E, and a function f : E → F , map f e is the sequence over F defined as

f (e 1 ) • f (e 2 ) • • • f (e n ) where ∀i ∈ [1, n] : f (e i ) ∈ F .

Component-Based Systems with Multiparty Interactions

An action of a CBS is an interaction i.e., a coordinated operation between certain atomic components. Atomic components are transition systems with a set of ports labeling individual transitions. Ports are used by components to communicate. Composite components are obtained from atomic components by specifying interactions.

An atomic component is endowed with a finite set of local variables X taking values in a domain Data, and it synchronizes with other components through ports. A port p[x p ], where x p ⊆ X, is defined by a port identifier p and some variables in a set x p .

Definition 1 (Atomic component). An atomic component is defined as a tuple (P, L, T, X) where P is the set of ports, L is the set of (control) locations, T ⊆ L × P × G(X) × F * (X) × L is the set of transitions, and X is the set of variables. G(X) denotes the set of Boolean expressions over X and F(X) the set of assignments of expressions over X to variables in X. For each transition τ = (l, p, g τ , f τ , l ) ∈ T , g τ is a Boolean expression over X (the guard of τ ), f τ ∈ {x := f x (X) | x ∈ X ∧ f x ∈ F * (X)} * : the computation step of τ , a sequence of assignments to variables.

The semantics of the atomic component is an LTS

(Q, P, →) where Q = L × [X → Data] is the set of states, and →= {((l, v), p(v p ), (l , v )) ∈ Q × P × Q | ∃τ = (l, p, g τ , f τ , l ) ∈ T : g τ (v) ∧ v = f τ (v/v p )} is the transition relation.
A state is a pair (l, v) ∈ Q, where l ∈ L, v ∈ [X → Data] is a valuation of the variables in X. The evolution of states (l, v) p(vp) -→ (l , v ), where v p is a valuation of the variables x p attached to port p, is possible if there exists a transition (l, p[x p ], g τ , f τ , l ), s.t. g τ (v) = true. As a result, the valuation v of variables is modified to We use the dot notation to denote the elements of atomic components. e.g., for a component B, B.P denotes the set of ports of the atomic component B, etc. Figure 2 depicts atomic components of system Task. Definition 2 (Interaction). An interaction a is a tuple (P a , F a ), where P a = {p i [x i ] | p i ∈ B i .P } i∈I is the set of ports s.t. ∀i ∈ I : P a ∩ B i .P = {p i } and F a is a sequence of assignment to the variables in ∪ i∈I x i . Variables attached to ports are purposed to transfer values between interacting components. When clear from the context, in the following examples, an interaction ({p[x p ]}, F a ) consisting of only one port p is noted p.

v = f τ (v/v p ).

Definition 3 (Composite component)

. A composite component γ(B 1 , . . . , B n ) is de- fined from a set of atomic components {B i } n
i=1 and a set of interactions γ.

A state q of γ(B 1 , . . . , B n ) is an n-tuple q = (q 1 , . . . , q n ), where q i = (l i , v i ) is a state of atomic component B i . The semantics of the composite component is an LTS (Q, γ, -→), where Q = B 1 .Q×. . .×B n .Q is the set of states, γ is the set of all possible interactions and -→ is the least set of transitions satisfying the following rule:

a = ({pi[xi]}i∈I , Fa) ∈ γ ∀i ∈ I : qi p i (v i ) -→ i q i ∧ vi = Fa i (v(X)) ∀i ∈ I : qi = q i (q1, . . . , qn) a -→ (q 1 , . . . , q n )
X is the set of variables attached to the ports of a, v is the global valuation, and F ai is the restriction of F to the variables of p i .

A trace is a sequence of states and interactions

(q 0 • a 1 • q 1 • • • a s • q s ) s.t.: q 0 = Init ∧ (∀i ∈ [1, s] : q i ∈ Q ∧ a i ∈ γ : q i-1 ai -→ q i ),
where Init ∈ Q is the initial state. The sequence of interactions is then defined as interactions(q 0 • a

1 • q 1 • • • a s • q s ) = a 1 • • • a s . The set of traces of composite component B is denoted by Tr(B). ex 13 ex 23 ex 12 n t f 2 r 2 f 3 r 3 f 1 r 1 Generator newtask deliver Worker 2 exec2 finish2 reset2 Worker 1 exec1 finish1 reset1 Worker 3 exec3 finish3 reset3 Fig. 3: Composite component of system Task Example 1 (Interaction, composite com- ponent). Figure 3 depicts the compos- ite component γ(Worker 1 , Worker 2 , Worker 3 , Generator ) of system Task. The set of interactions is γ = {ex 12 , ex 13 , ex 23 , r 1 , r 2 , r 3 , f 1 , f 2 , f 3 , n t }. For instance, we have ex 12 = ({deliver , exec 1 , exec 2 }, [ ]).
One of the possible traces2 of system Task is: (free, free, free, hold ) • ex 12 •(done, done, free, delivered ) • n t • (done, done, free, hold ) s.t. from the initial state (free, free, free, hold ), where workers are at location free and task generator is ready to deliver a task, interaction ex 12 is fired and Worker 1 and Worker 2 move to location done and Generator moves to location delivered . Then, a new task is generated by the execution of interaction n t so that Generator moves to location hold .

Monitoring Multi-Threaded CBSs with Partial-State Semantics

The semantics defined in Sec. 3 is referred to as the global-state semantics of CBSs because each state of the system is defined in terms of the local states of components, and, all local states are defined. In this section, we consider the partial-state semantics where the states of a system may contain undefined local states because of the concurrent execution of components.

Partial-State Semantics

To model concurrent behavior, we associate a partial state model to each atomic component. In global-state semantics, one does not distinguish the beginning of an interaction (or a transition) from its completion. That is, the interactions and transitions of a system execute atomically and sequentially. Partial states and the corresponding internal transitions are needed for modeling non-atomic executions. Atomic components with partial states behave as atomic components except that each transition is decomposed into a sequence of two transitions: a visible transition followed by an internal β-labeled transition (aka busy transition). Between these transitions, a so-called busy location is added. Below, we define the transformation of a component with globalstate semantics to a component with partial-state semantics (extending the definition in [START_REF] Basu | Distributed semantics and implementation for systems with interaction and priority[END_REF] with variables, guards, and computation steps on transitions). Definition 4 (Components with partial states). The partial-state version of atomic component B = (P, L, T, X) is

B ⊥ = (P ∪ {β}, L ∪ L ⊥ , T ⊥ , X), where β / ∈ P is a special port, L ⊥ = {l ⊥ t | t ∈ T } (resp. L) is the set of busy locations (resp. ready location) s.t. L ⊥ ∩ L = ∅, T ⊥ = {(l, p, g τ , [ ], l ⊥ τ ), (l ⊥ τ , β, true, f τ , l ) | ∃τ = (l, p, g τ , f τ , l ) ∈ T } is a set of transitions.
Assuming some atomic components with partial-state semantics

B ⊥ 1 , . . . , B ⊥ n , we construct a composite component B ⊥ = γ ⊥ (B ⊥ 1 , ..., B ⊥ n ) where γ ⊥ = γ ∪ {{β i }} n i=1
, and {{β i }} n i=1 is the set of busy interactions. The notions and notation related to traces are lifted to components with partial-state semantics in the natural way. We extend the definition of interactions to traces in partial-state semantics s.t. β i∈ [1,n] are filtered out.

⊥ (Worker ⊥ 1 , Worker ⊥ 2 , Worker ⊥ 3 , Generator ⊥ ),
where each Worker ⊥ i for i ∈ [START_REF] Basu | Distributed semantics and implementation for systems with interaction and priority[END_REF][START_REF] Bauer | Comparing LTL semantics for runtime verification[END_REF] is identical to the component in Fig. 4b and Generator ⊥ is the component in Fig. 4a. We represent each busy location l ⊥ as ⊥. It is possible to show that the partial-state system is a correct implementation of the global-state system, that is, the two systems are (weakly) bisimilar (cf. [START_REF] Basu | Distributed semantics and implementation for systems with interaction and priority[END_REF], Theorem 1). Weak bisimulation relation R is defined between the set of states of the model in global-state semantics (i.e., Q) and the set of states of its partial-state

model (i.e., Q ⊥ ), s.t. R = {(q, r) ∈ Q×Q ⊥ | r β * -→ q}.
Any global state in partial-state semantics model is equivalent to the corresponding global state in global-state semantics model, and any partial state in partial-state semantics model is equivalent to the successor global state obtained after stabilizing the system by executing busy interactions. In the sequel, we consider a CBS with global-state semantics B and its partial-state semantics version B ⊥ . Intuitively, from any trace of B ⊥ , we want to reconstruct on-thefly the corresponding trace in B and evaluate a property which is defined over global states of B.

Witness Relation and Witness Trace

We define the notion of witness relation between traces in global-state semantics and traces in partial-state semantics, based on the bisimulation between B and B ⊥ . Any trace of B ⊥ is related to a trace of B, i.e., its witness. The witness trace allows to monitor the system in partial-state semantics (thus benefiting from the parallelism) against properties referring to the global behavior of the system.

q 0 q 0 • • • • • • • • • • • • q 1 • • • qi-1 q i • • • β β β
Trace in partial-state semantics Witness trace in global-state semantics

R a 1 β a 2 β a i β a i+1 a 1 R R R a 2 a i a i+1 R R R R
Fig. 5: Witness trace built using weak bisimulation (R)

(
For (σ 1 , σ 2 ) ∈ W, • (σ 1 • a • q 1 , σ 2 • a • q 2 ) ∈ W, if a ∈ γ and (q 1 , q 2 ) ∈ R; • (σ 1 , σ 2 • β • q 2 ) ∈ W, if (last(σ 1 ), q 2 ) ∈ R. If (σ 1 , σ 2 ) ∈ W, we say that σ 1 is a witness trace of σ 2 .
Suppose that the witness relation relates a trace in partial-state semantics σ 2 to a trace in global-state semantics σ 1 . The states obtained after executing the same interaction in the two systems are bisimilar. Moreover, any move through a busy interaction in B ⊥ preserves the bisimulation between the state of σ 2 followed by the busy interaction in B ⊥ and the last state of σ 1 in B.

Example 3 (Witness relation and trace). Figure 5 illustrates the witness relation. State q 0 is the initial state of B and B ⊥ . In the trace of B ⊥ , gray circles after each interaction represent partial states which are bisimilar to the global state that comes after the corresponding trace of B.

Let us consider σ 2 as a trace of system Task with partial-state semantics depicted in Fig. 6 where σ 2 = (free, free, free, hold

) • ex 12 •(⊥, ⊥, free, ⊥) • β 4 • (⊥, ⊥, free, delivered ) • n t • (⊥, ⊥, free, ⊥).
The witness trace corresponding to trace σ 2 is (free, free, free, hold ) • ex 12 • (done, done, free, delivered ) • n t • (done, done, free, hold ).

Property 1 states that any trace in partial-state semantics and its witness trace have the same sequence of interactions. Property 2 states that any trace in the partial-state semantics has a unique witness trace in the global-state semantics.

Property 1. ∀(σ 1 , σ 2 ) ∈ W, interactions(σ 1 ) = interactions(σ 2 ). Property 2. ∀σ 2 ∈ Tr(B ⊥ ), ∃! σ 1 ∈ Tr(B), (σ 1 , σ 2 ) ∈ W. Following Property2, we note W(σ 2 ) = σ 1 when (σ 1 , σ 2 ) ∈ W.
Note that, when running a system in partial-state semantics, the global state of the witness trace after an interaction a is not known until all the components involved in a have reached their ready locations after the execution of a. Nevertheless, even in nondeterministic systems, this global state is uniquely defined and consequently there is always a unique witness trace (that is, non-determinism is resolved at runtime).

Construction of the Witness Trace

Given a trace in partial-state semantics, the witness trace is computed using function RGT (Reconstructor of Global Trace).

Definition 6 (Function RGT ). Function RGT : Tr(B ⊥ ) -→ pref(Tr(B)) is defined as RGT(σ) = discriminant(acc(σ)), where:

-acc : Tr(B ⊥ ) -→ Q • (γ • Q) * • (γ • (Q ⊥ \Q)) * is defined as: • acc(Init) = Init, • acc(σ • a • q) = acc(σ) • a • q for a ∈ γ, • acc(σ • β • q) = map [x → upd(q, x)] (acc(σ)) for β ∈ {{β i }} n i=1 ; -discriminant : Q • (γ • Q) * • (γ • (Q ⊥ \Q)) * -→ pref(Tr(B)) is defined as: discriminant(σ) = max ({σ ∈ pref(σ) | last(σ ) ∈ Q}) with upd : Q ⊥ × (Q ⊥ ∪ γ) -→ Q ⊥ ∪ γ defined as: -upd((q 1 , . . . , q n ), a) = a, for a ∈ γ,
upd (q 1 , . . . , q n ), (q 1 , . . . , q n ) = (q 1 , . . . , q n ),

where ∀k ∈ [1, n], q k = q k if (q k / ∈ Q ⊥ k ) ∧ (q k ∈ Q ⊥ k ) q k otherwise.
Function RGT uses sub-functions acc and discriminant. First, acc takes as input a trace in partial-state semantics σ, removes β interactions and the partial states after β. Function acc uses the (information in the) partial state after β interactions in order to update the partial states using function upd. Then, function discriminant returns the longest prefix of the result of acc corresponding to a trace in global-state semantics.

Note that, because of the inductive definition of function acc, the input trace can be processed step by step by function RGT which can incrementally generate the witness trace of a running system by monitoring interactions and partial states of components.

Example 4 (Applying function RGT). Table 1 illustrates Definition 6 on one trace of system Task with initial state (free, free, free, hold ) followed by interactions ex 12 , β 4 , n t , β 2 , and β 1 . At step 0, the outputs of functions acc and discriminant are equal to the initial state. At step 1, the execution of interaction ex 12 adds ex 12 •(⊥, ⊥, free, ⊥) to traces σ and acc(σ). At step 2, the state after β 4 has fresh information on component Generator which is used to update the existing partial states, so that (⊥, ⊥, free, ⊥) is updated to (⊥, ⊥, free, delivered ). At step 5, Worker 1 becomes ready after β 1 , and the partial state (⊥, done, free, delivered ) in the intermediate step is updated to the global state (done, done, free, delivered ), therefore it appears in the output trace.

The following proposition states that applying function RGT on a trace in partial-state semantics produces the longest possible prefix of the corresponding witness trace with respect to the current trace of the partial-state semantics model.

last(σ) ∈ Q =⇒ RGT(σ) = W(σ) ∧ last(σ) / ∈ Q =⇒ RGT(σ) = W(σ ) • a, with σ = min {σ p ∈ Tr(B ⊥ ) | ∃a ∈ γ, ∃σ ∈ Tr(B ⊥ ) : σ = σ p • a • σ ∧ ∃i ∈ [1, n] : (B i .P ∩ a = ∅) ∧ (∀j ∈ [1, length(σ )] : β i = σ (j))}
Theorem 1 distinguishes two cases:

• When the last state of a system is a global state (last(σ) ∈ Q), none of the components is in a busy location. Moreover, function RGT has sufficient information to build the corresponding witness trace (RGT(σ) = W(σ)). • When the last state of a system is a partial state, at least one component is in a busy location and function RGT can not build a complete witness trace because it lacks information on the current state of such components. It is possible to decompose the input sequence σ into two parts σ and σ separated by an interaction a. The separation is made on the interaction a occurring in trace σ s.t., for the interactions occurring after a (i.e., in σ ), at least one component involved in a has not executed any β transition (which means that this component is still in a busy location). Note that it may be possible to split σ in several manners with the above description. In such a case, function RGT computes the witness for the smallest sequence σ (w.r.t. prefix ordering) as above because it is the only sequence for which it has information regarding global states. Note also that such splitting of σ is always possible as last(σ) / ∈ Q implies that σ is not empty, and σ can be chosen to be .

In both cases, RGT returns the maximal prefix of the corresponding witness trace that can be built with the information contained in the partial states observed so far.

Instrumentation of Atomic Components

Given an atomic component with partial-state semantics as per Definition 4, we instrument this atomic component s.t. it is able to transfer its state through port β, each time the component moves out from a busy location.

Definition 7 (Instrumenting an atomic component). Given an atomic component in partial-state semantics

B ⊥ = (P ∪ {β}, L ∪ L ⊥ , T ⊥ , X) with initial location l 0 ∈ L, we define a new component B r = (P r , L ∪ L ⊥ , T r , X r ) where: • X r = X ∪ {loc}, loc is initialized to l 0 ; • P r = P ∪ {β r }, with β r = β[X r ]; • T r = {(l, p, g τ , [ ], l ⊥ τ ), (l ⊥ τ , β, true, f τ ; [loc := l ], l ) | (l, p, g τ , [ ], l ⊥ τ ), (l ⊥ τ , β, true, f τ , l ) ∈ T ⊥ }.
In X r , loc is a variable containing the current location. X r is exported through port β. An assignment is added to the computation step of each transition to record the location.

Example 5 (Instrumenting an atomic component). Figure 7 shows the instrumented version of atomic components in system Task (depicted in Fig. 4). Definition 8 (RGT atom). Component RGT is defined as (P , L, T , X) where: RGT

Creating a New Atomic Component to Reconstruct Global States

Let us consider

B ⊥ = γ ⊥ (B ⊥ 1 , . . . , B ⊥ n ) with
• X = i∈[1,n] {B r i .X r } i∈[1,n] {B r i .X r c } ∪ {gs a | a ∈ γ} ∪ {(z 1 , . . . , z n )} ∪ {V, v,
ex 13 ex 23 f 3 r 3 f 2 r 2 f 1 r 1 ex
(e1 ∧ e2 ∧ e3) pintern , [print "bad"] (¬e1 ∨ ¬e2 ∨ ¬e3)
pa, for a ∈ γ Fig. 8: Monitored version of system Task

• P = i∈[1,n] {β i [B r i .X r ]} ∪ {p a [∅] | a ∈ γ} ∪ {p a [ i∈[1,n] {B r i .X c }] | a ∈ γ}. • L = {l} is a set with one control location. • T = T new ∪ T upd ∪ T out , where: T new = {(l, p a , true, new(a), l) | a ∈ γ}, T upd = {(l, β i , a∈γ (¬gs a ), upd(i), l) | i ∈ [1, n]}, T out = {(l, p a , gs a , get, l) | a ∈ γ}.
For space reasons, we only overview the description of atom RGT and do not provide the internal algorithms. Full and formal details can be found in [START_REF] Nazarpour | Monitoring multi-threaded component-based systems[END_REF]. A global state is encoded as a tuple consisting of the valuation of variables and the location for each atomic component. After a new interaction gets fired, component RGT builds a new tuple using the current states of components. Component RGT builds a sequence with the generated tuples. The stored tuples are updated each time the state of a component is updated. Following Definition 7, atomic components transfer their states through port β each time they move from a busy location to a ready location. RGT reconstructs global states from these received partial states, stores them in variable V and delivers them through the dedicated ports.

Example 6 (RGT atom). Figure 8 depicts the component RGT for system Task. For space reasons, only one instance of each type of transitions is shown. At runtime, RGT produces the sequence of global states in the right-most column of Table 1.

Connections

After building component RGT (see Definition 8), and instrumenting atomic components (see Definition 7), we modify all interactions and define new interactions to build a new transformed composite component. To let RGT accumulate states of the system, first we transform all the existing interactions by adding a new port to communicate with component RGT, then we create new interactions that allow RGT to deliver the reconstructed global states of the system to a runtime monitor.

Given a composite component

B ⊥ = γ ⊥ (B ⊥ 1 , . . . , B ⊥ n ) with corresponding com- ponent RGT and instrumented components B r = (P ∪ {β r }, L ∪ L ⊥ , T r , X r ) s.t. B r = B r i ∈ {B r 1 , • • • , B r n }, we define a new composite component. Definition 9 (Composite component transformation). For a composite component B ⊥ = γ ⊥ (B ⊥ 1 , . . . , B ⊥ n ), we introduce a corresponding transformed component B r = γ r (B r 1 , . . . , B r n , RGT ) s.t. γ r = a r γ ⊥ ∪ a m where: • a r γ ⊥ = {a r | a ∈ γ ⊥ } is the set of transformed interactions with: ∀a ∈ γ ⊥ , a r = a ∪ {RGT.p a } if a ∈ γ, a ∪ {RGT.β i } otherwise (a ∈ {{β i }} n i=1 ). • a m is a set of new interactions s.t. a m = {a | a ∈ γ}, where ∀a ∈ γ, a =
{RGT.p a } is the corresponding unary interaction.

For each interaction a ∈ γ ⊥ , we associate a transformed interaction a r which is the modified version of interaction a s.t. a corresponding port of component RGT is added to a. Instrumenting interaction a ∈ γ does not modify sequence of assignment F a , whereas instrumenting busy interactions a ∈ {{β i }} n i=1 adds assignments to transfer attached variables of port β i to the component RGT. The set a m is the set of all unary interactions a associated to each existing interaction a ∈ γ in the system.

Example 7 (Transformed composite component). Figure 8 shows the transformed composite component of system Task. The goal of building a for each interaction a is to enable RGT to connect to a runtime monitor. Upon the reconstruction of a global state corresponding to interaction a ∈ γ, the corresponding interaction a delivers the reconstructed global state to a runtime monitor.

Correctness of the Transformations and Monitoring

Combined together, the transformations preserve the semantics of the initial model as stated by the following propositions. Intuitively, component RGT (cf. Definition 8) implements function RGT (cf. Definition 6). Reconstructed global states are transferable through the ports p a∈γ . If interaction a happens before interaction b, then in component RGT, port p a which contains the reconstructed global state after executing a will be enabled before port p b : the total order between executed interactions is preserved.

Proposition 1 (Correctness of component RGT). For any execution, at any time, variable RGT .V encodes the witness trace of the current execution: RGT .V is a sequence of tuples where each tuple consists of the state and the interaction that led to this state, in the same order as they appear on the witness trace.

For each trace in partial-state semantics, component RGT produces the witness trace in the initial model, as stated by the following theorem.

Theorem 2 (Transformation correctness). γ ⊥ (B ⊥ 1 , ..., B ⊥ n ) ∼ γ r (B r 1 , ..., B r n , RGT ).

Connecting a monitor. Using [START_REF] Falcone | Runtime verification of component-based systems in the BIP framework with formally-proved sound and complete instrumentation[END_REF], one can monitor a system with partial-state semantics with the previous transformations by plugging a monitor to component RGT through the dedicated ports. At runtime, such monitor will i) receive the sequence of reconstructed global states corresponding to the witness trace, ii) preserve the concurrency of the system, and iii) state verdicts on the witness trace.

Example 8 (Monitoring system Task). Figure 8 depicts the transformed system Task with a monitor (for the homogeneous distribution of the tasks among the workers) where e 1 , e 2 , and e 3 are events related to the pairwise comparison of the number of executed tasks by Worker s. For i ∈ [START_REF] Basu | Distributed semantics and implementation for systems with interaction and priority[END_REF][START_REF] Bauer | Comparing LTL semantics for runtime verification[END_REF], event e i evaluates to true whenever |x i mod 3+1 -x i mod 3 | is lower than 3 (for this example). 1) is sent by component RGT to the monitor which in turn produces the sequence of verdicts c • c (where c is verdict currently good, see [START_REF] Bauer | Comparing LTL semantics for runtime verification[END_REF][START_REF] Falcone | What can you verify and enforce at runtime?[END_REF]).

Implementation and Performance Evaluation

We present some case studies on executable BIP systems conducted with RVMT-BIP, a tool integrated in the BIP tool suite [START_REF] Basu | Modeling heterogeneous real-time components in BIP[END_REF].

Case Study 1: Demosaicing Demosaicing is an algorithm for digital image processing used to reconstruct a full color image from the incomplete color samples output from an image sensor. The model contains ca. 1,000 lines of code, consists of 26 atomic components interacting through 35 interactions. We consider two specifications related to process completion: i) Internal demosaicing units should finish their process before post-demosaicing starts processing (ϕ 1 ). ii) Internal demosaicing units should not start demosaicing process before pre-demosaicing finishes its process (ϕ 2 ).

Case Study 2: Task Management We consider our running example system Task and a specification of the homogeneous distribution of the tasks among the workers (ϕ 3 ).

Evaluation Principles For each system, and all its properties, we synthesize a BIP monitor following [START_REF] Falcone | Runtime verification of component-based systems in the BIP framework with formally-proved sound and complete instrumentation[END_REF] and combine it with the CBS output from RVMT-BIP. We obtain a new CBS with corresponding RGT and monitor components. We run each system by using various number of threads and observe the execution time. Executing these systems with a multi-threaded controller results in a faster run because the systems benefit from the parallel threads. Additional steps are introduced in the concurrent transitions of the system. Note, these are asynchronous with the existing interactions and can be executed in parallel. These systems can also execute with a single-threaded controller which forces them to run sequentially. Varying the number of threads allows us to assess the performance of the (monitored) system under different degrees of parallelism. In particular, we expected the induced overhead to be insensitive to the degree of parallelism. For instance, an undesirable behavior would have been to observe a performance degradation (and an overhead increase) which would mean either that the monitor sequentializes the execution or that the monitoring infrastructure is not suitable for multi- threaded systems. We also extensively tested the functional correctness of RVMT-BIP, that is whether the verdicts of the monitors are sound and complete.

Results (cf. Table 2) Each time measurement is an average value obtained after 100 executions. Column # interactions shows the number of functional steps of system. Columns no monitor reports the execution time of the systems without monitors when varying the number of threads. Columns with monitor reports the execution time of the systems with monitors when varying the number of threads, the number of additional interactions and overhead induced by monitoring. Column events indicates the number of reconstructed global states (events sent to the associated monitor). As shown in Table 2, using more threads reduces significantly the execution time in both the initial and transformed systems. Comparing the overheads according to the number of threads shows that the proposed monitoring technique i) does not restrict the performance of parallel execution and ii) scales up well with the number of threads. RV-BIP vs. RVMT-BIP. To illustrate the advantages of monitoring multi-threaded systems with RVMT-BIP, we compared it to RV-BIP [START_REF] Falcone | Runtime verification of component-based systems in the BIP framework with formally-proved sound and complete instrumentation[END_REF]. Table 3 shows the results of a performance evaluation of monitoring Demosaicing and Task. RV-BIP induces a cheap overhead of 6.91% with one thread and a huge overhead of 46.1% (which is mainly caused by globally-synchronous extra interactions introduced by RV-BIP) with two threads, whereas according to Table 2, the overhead induced by RVMT-BIP with two threads is 0.73%. The induced overhead is even better than the overhead induced when monitoring the single-threaded version of the system which is 2.67%. As can be seen in Table 3, RVMT-BIP outperforms RV-BIP when monitoring Demosaicing. The latter does not take any advantage of the parallel execution. This clearly demonstrates the advantages of our monitoring approach over [START_REF] Falcone | Runtime verification of component-based systems in the BIP framework with formally-proved sound and complete instrumentation[END_REF].

Related Work

Several approaches are related to the one in this paper, as they either target CBSs or address the problem of concurrently runtime verifying systems.

Runtime verification of single-threaded CBSs. In [START_REF] Falcone | Runtime verification of component-based systems in the BIP framework with formally-proved sound and complete instrumentation[END_REF], we proposed a first approach for the runtime verification of CBSs. The approach takes a CBS and a regular property as input and generates a monitor implemented as a component which is then integrated within an existing CBS. At runtime, the monitor consumes the global trace (i.e., sequence of global states) and yields verdicts regarding property satisfaction. The technique in [START_REF] Falcone | Runtime verification of component-based systems in the BIP framework with formally-proved sound and complete instrumentation[END_REF] only efficiently handles CBSs with sequential executions: if applied to a multi-threaded CBS, the monitor would sequentialize completely the execution. Hence, the approach proposed in this paper can be used in conjunction with the approach in [START_REF] Falcone | Runtime verification of component-based systems in the BIP framework with formally-proved sound and complete instrumentation[END_REF] when dealing with multi-threaded CBSs: a monitor as synthesized in [START_REF] Falcone | Runtime verification of component-based systems in the BIP framework with formally-proved sound and complete instrumentation[END_REF] can be plugged to component RGT which is reconstructing the global states of the system. Decentralized runtime verification. The approaches in [START_REF] Bauer | Decentralised LTL monitoring[END_REF][START_REF] Falcone | Efficient and generalized decentralized monitoring of regular languages[END_REF] decentralize monitors for linear-time specifications on a system made of synchronous black-box components that cannot be executed concurrently. Moreover, monitors only observe the outside visible behavior of components to evaluate the formulas at hand. The decentralized monitor evaluates the global trace by considering the locally-observed traces obtained by local monitors. To locally detect global violations/satisfactions, local monitors need to communicate, because their trace are only partial w.r.t. the global behavior of the system. Monitoring safety properties in concurrent systems. The approach in [START_REF] Sen | Decentralized runtime analysis of multithreaded applications[END_REF] addresses the monitoring of asynchronous multi-threaded systems against temporal logic formulas expressed in MTTL. MTTL augments LTL with modalities related to the distributed/multi-threaded nature of the system. The monitoring procedure in [START_REF] Sen | Decentralized runtime analysis of multithreaded applications[END_REF] takes as input a safety formula and a partially-ordered execution of a parallel asynchronous system, and then predicts a potential property violation on one of the causally-consistent interleavings of the observed execution. Our approach mainly differs from [START_REF] Sen | Decentralized runtime analysis of multithreaded applications[END_REF] in that we target CBSs. Moreover, we assume a central scheduler and we only need to monitor the unique causally-consistent global trace with the observed partial trace. Also, we do not place any expressiveness restriction on the formalism used to express properties. Parallel runtime verification of monolithic sequential programs. Berkovich et al. [START_REF] Berkovich | GPU-based runtime verification[END_REF] introduce parallel algorithms to speed up the runtime verification of sequential programs against complex LTL formulas using a graphics processing unit (GPU). Monitoring threads directly execute on the GPU. The approach in [START_REF] Berkovich | GPU-based runtime verification[END_REF] is not tailored to CBSs and is a complementary technique that adds significant computing power to the system to handle the monitoring overhead. Note that, as shown by our experiments, our approach preserves the performance of the monitored system. Finally, our approach is not bound to any particular logic, and allows for Turing-complete monitors.

Future Work

A first direction is to consider monitoring for fully decentralized and distributed models where a central controller does not exist. For this purpose, we intend to make controllers collaborating in order to resolve conflicts in a distributed fashion. This setting should rely on the distributed semantics of CBSs [START_REF] Bonakdarpour | A framework for automated distributed implementation of component-based models[END_REF]. A lot of work has been done in order to monitor properties on a distributed (monolithic) systems; e.g., [START_REF] Sen | Formal verification of simulation traces using computation slicing[END_REF] for online monitoring of CTL properties, [START_REF] Mostafa | Decentralized runtime verification of LTL specifications in distributed systems[END_REF] for online monitoring of LTL properties, [START_REF] Sen | Detecting temporal logic predicates in distributed programs using computation slicing[END_REF] for offline monitoring of properties expressed in a variant of CTL, and [START_REF] Tomlinson | Monitoring functions on global states of distributed programs[END_REF] for online monitoring of global-state predicates. In the future, we plan to adapt these approaches to the context of CBSs. Another possible direction is to extend the proposed framework for timed components and timed specifications as presented in [START_REF] Basu | Modeling heterogeneous real-time components in BIP[END_REF].

Fig. 2 :

 2 Fig. 2: Atomic components

Fig. 4 :

 4 Fig. 4: Atomic components of Task with partial-states

  Instrumented component Worker r

Fig. 7 :

 7 Fig. 7: Instrumented atomic components of system Task

  m}, where B r i .X r c is a set containing a copy of the variables in B r i .X r .

  , a BIP system with global-state semantics S g (sequential model), is (weakly) bisimilar with the corresponding partial-state model S p (concurrent model) noted S g ∼ S p . Moreover, S p generally

		BIP system Sg			Transformation [1]	BIP system Sp
					(β transitions)
		Execution Trace Global-state semantics	Global states		Execution Trace Partial-state semantics	Transformation w.r.t ϕ
	Property ϕ on global states	Monitor synthesis [9]	Runtime Monitor	Global states	Partial-state semantics BIP system Spg
						Witness Trace

Table 1 :

 1 Values of function RGT for a sample input

	Step Input trace in partial semantics, σ	Intermediate step, acc(σ)	Output trace in global semantics, RGT(σ)
	0	(free, free, free, hold )	(free, free, free, hold )	(free, free, free, hold )
	1	(free, free, free, hold ) • ex 12 • (⊥, ⊥, free, ⊥)	(free, free, free, hold ) • ex 12 • (⊥, ⊥, free, ⊥)	(free, free, free, hold ) • ex 12
	2	(free, free, free, hold ) • ex 12 • (⊥, ⊥, free, ⊥) • β4• (⊥, ⊥, free, delivered )	(free, free, free, hold ) • ex 12 • (⊥, ⊥, free, delivered )	(free, free, free, hold ) • ex 12
	3	(free, free, free, hold ) • ex 12 • (⊥, ⊥, free, ⊥) • β4• (⊥, ⊥, free, ⊥) (⊥, ⊥, free, delivered ) • nt•	(free, free, free, hold ) • ex 12 • (⊥, ⊥, free, ⊥) (⊥, ⊥, free, delivered ) • nt•	(free, free, free, hold ) • ex 12
		(free, free, free, hold ) • ex 12 •
		(⊥, ⊥, free, ⊥) • β4•	(free, free, free, hold ) • ex 12 •
	4	(⊥, ⊥, free, delivered ) • nt•	(⊥, done, free, delivered ) • nt•	(free, free, free, hold ) • ex 12
		(⊥, ⊥, free, ⊥) • β2•	(⊥, done, free, ⊥)
		(⊥, done, free, ⊥)

5

(free, free, free, hold

) • ex 12 • (⊥, ⊥, free, ⊥) • β4• (⊥, ⊥, free, delivered ) • nt• (⊥, ⊥, free, ⊥) • β2• (⊥, done, free, ⊥) • β1• (done,

done, free, ⊥) (free, free, free, hold ) • ex 12 • (done, done, free, delivered ) • nt• (done, done, free, ⊥) (free, free, free, hold ) • ex 12 • (done, done, free, delivered ) • nt Theorem 1 (Computation of the witness with RGT). ∀σ ∈ Tr(B ⊥ ) :

  partial-state semantics, s.t.: • γ is the set of interactions in the corresponding composite component with globalstate semantics with γ = γ ⊥ \ {{β i }} n i=1 , and • the corresponding instrumented atomic components B r 1 , . . . , B r n have been obtained through Definition 7 s.t. B r i is the instrumented version of B ⊥ i . We define a new atomic component, called RGT, which is in charge of accumulating the global states of the system B ⊥ . Component RGT is an operational implementation as a component of function RGT (Definition 6).

  Component Monitor evaluates (e 1 ∧ e 2 ∧ e 3 ) upon the reception of a new global state from RGT and emits the associated verdict till reaching bad state ⊥. The global trace (free, free, free, hold ) • ex 12 •(done, done, free, delivered ) • n t (see Table

Table 2 :

 2 Results of monitoring Demosaicing and Task with RVMT-BIP

	system	# interactions no monitor				with monitor
			thread time (s) specification # extra interactions events thread time (s) overhead (%)
			1	67.97		ϕ1	6,800	4,399	1 3	68.706 41.245	1.07 1.53
	Demosaicing	8,400	3	40.62	Process completion				10 29.521 1 69.116	1.24 1.67
			10	29.15		ϕ2	2,200	1,599	3 10 29.251 41.235	1.51 0.31
	Task (100,000 tasks)	399,999	1 2	117.96 72.32	Task distribution	ϕ3	200,198	100,197	1 2	121.12 72.85	2.67 0.73

Table 3 :

 3 Results of monitoring with RV-BIP

	system	# interactions no monitor			with monitor
			thread time (s) specification # extra interactions thread time (s) overhead (%)
	Demosaicing	8,400	1 10	67.97 29.15	Process completion	ϕ2	3,202	1 10 172.31 175.83	158.6 491.1
	Task (100,000 tasks)	399,999	1 2	117.96 72.32	Task distribution	ϕ3	177,611	1 2	126.11 105.66	6.91 46.1

RVMT-BIP is available for download at[START_REF] Nazarpour | Runtime Verification of Multi-Threaded BIP[END_REF].

For the sake of simpler notation, we represent a state by its location.

Acknowledgement. The authors are supported by the Artemis ARROWHEAD project under grant agreement number 332987 (ARTEMIS/ECSEL Joint Undertaking, supported by the European Commission and French Public Authorities). The work reported in this article is in the context of the COST Action ARVI IC1402, supported by COST (European Cooperation in Science and Technology).