Yliès Falcone
email: ylies.falcone@ujf-grenoble.fr1

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

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.

Introduction

Component-based Systems. A component-based approach consists in building complex systems by composing components (building blocks). This confers numerous advantages (e.g., productivity, incremental construction, compositionality) that allow one to deal with complexity in the construction phase. Componentbased systems (CBS) are desirable because they allow reuse of sub-systems as well as their incremental modification without requiring global changes. The development of CBS requires methods and tools supporting a concept of architecture which characterizes the coordination between components. An architecture structures a system and involves components and relationships between the externally visible properties of those components. The global behavior of a system can, in principle, be inferred from the behavior of its components and its architecture. Component-based design is based on the separation between coordination and computation. Systems are built from units executing sequential code insulated from concurrent execution issues. The isolation of coordination mechanisms allows a global treatment and analysis on coordination constraints between components even if local computations on components are not visible (i.e., components are "black boxes").

BIP (Behavior Interaction Priority

). BIP is a general framework supporting rigorous design. BIP uses a dedicated language and an associated toolset supporting the design flow. The BIP language allows building complex systems by coordinating the behavior of a set of atomic components. Behavior is described with Labelled Transition Systems (LTS) extended with data and functions written in C. The description of coordination between components is layered. The first layer describes the interactions between components. The second layer describes dynamic priorities between the interactions and is used also to express scheduling policies. The combination of interactions and priorities characterizes the overall architecture of a system and confers strong expressiveness that cannot be matched by other existing formalism dedicated to CBS [?].

Moreover, BIP has a rigorous operational semantics: the behavior of a composite component is formally described as the composition of the behaviors of its atomic components. This allows a direct relation between the underlying semantic model and its implementation.

Runtime verification (monitoring). Runtime Verification (RV) [?,?,?] is an effective technique to ensure, at runtime, that a system respects or meets a desirable behavior. It can be used in numerous application domains, and more particularly when integrating together unreliable software components. In RV, a run of the system under scrutiny is analyzed incrementally using a decision procedure: a monitor. This monitor may be generated from a user-provided high level specification (e.g., a temporal formula, an automaton). This monitor aims to detect violation or satisfaction w.r.t. the given specification. Generally, it is a state machine processing an execution sequence (step by step) of the monitored program, and producing a sequence of verdicts (truth-values taken from a truth-domain) indicating specification fulfillment or violation. Recently [?] a new framework has been introduced for runtime verification. This expressive framework, leveraged by a finite-trace semantics (initially proposed in [?]) and an expressive truth-domain, allows to monitor all specifications expressing a linear temporal behavior. For a monitor to be able to observe runs of the system, the system should be instrumented in such a way that at runtime, the program sends relevant events that are consumed by the monitor. Usually, one of the main challenges when designing an RV framework is its performance. That is, adding a monitor in the system should not deteriorate executions of the initial system time and memory wise.

Motivations for using monitoring to validate component-based systems. As is the case with monolithic systems, monitoring is a complementary technique to validate the behavior of component-based systems.

Monitoring has several advantages when compared to static validation techniques. Compared to static analysis, monitoring allows to check more expressive behavioral specifications. Moreover, monitoring does not rely on abstracting or over-approximating the state-space, and thus does not produce false positives. Compared to model-checking, monitoring is less sensitive to the state-explosion problem which is rapidly occurring when composing the behavior of several components. Compared to compositional verification techniques, monitoring remains applicable for BIP component-based systems (where external functions can be called). Regarding BIP systems, classical model-checking techniques rapidly become unusable because of the state-explosion problem. Consequently, the currently available verification techniques are based on compositional/incremental verification. However, in the BIP framework, compositional verification is currently limited to the verification of safety properties, and, more expressive properties such as liveness properties remain out of the scope. In Section ??, we provide a more detailed comparison with static-verification techniques.

Challenges in monitoring component-based systems and BIP systems. Contrarily to monolithic systems (written for instance in Java), component-based systems are not endowed with an automatic and effective instrumentation technique. An automatic instrumentation technique allows the programmer to only indicate points of observation (in a more or less abstract fashion) and automatically adds observation code at relevant places in the original program. An effective instrumentation techniques ensures that the performance of the instrumented program is close to the performance of the original program. Such an instrumentation technique is required when designing or implementing a runtime verification framework for a target systemdomain. Consequently, we should design an instrumentation technique that should enjoy several features.

As is the case with monolithic system, we require an automatic and efficient instrumentation technique.

Moreover, we require a high-level of confidence on its correctness. The instrumentation technique should not alter the behavior of the initial system. Existing RV frameworks attempt to preserve the behavior of the system by performing only observations. For instance, using aspect-oriented programming, the used aspects only pick-up events without modifying the control-flow of the original program. However, in the context of component-based systems, such a desirable correctness property is harder to obtain. Indeed, to monitor a component-based system, one needs to add the monitor as a new component, which is allowed to observe the system by adding interactions. Such interactions should be inserted carefully because they could not only modify the existing interactions but also modify the internal behaviors of existing components. Finally, we aim at providing a method that can be used in critical systems and thus require a high-level of confidence on the proposed instrumentation technique. Consequently, the designed instrumentation technique should be defined formally and its correctness formally proved.

Our approach (informal view). Let us depict a high-level view of our approach. On the one hand, we consider an initial component-based system C = (B 1 , . . . , B n ) built over existing atomic components B 1 , . . . , B n . The atomic components are designed independently regarding their data and their behavior but they can interact and synchronize at runtime. We assume a global clock operating on C in such a way that, at each execution step, each atomic component can perform one action independently. When components are interacting together, we assume this communication to be reliable and do not consider any issue regarding privacy or security. On the other hand, a property ϕ specifies the desired runtime behavior of C. The property ϕ is associated to an abstract decision procedure (a monitor) M ϕ which is generated using standard monitor synthesis techniques. Verdicts over the behavior are based on an expressive truth-domain as in [?].

Verdicts can indicate current satisfaction and violation, or, definitive satisfaction or violation (in which case no monitoring is needed).

We shall transform C into a new component-based system C = (B 1 , . . . , B n , M ϕ ). C contains a monitor M ϕ as a component generated from M ϕ . Atomic components are instrumented (B i transformed to B i ) to interact with M ϕ . Moreover, we require some behavioral equivalence between the initial and transformed systems. This behavioral equivalence states that, up to some behavioral equivalence relation, not only the sets of possible behaviors in the initial and transformed system are equivalent, but, in addition, if the initial system produces any execution, then the transformed system produces an equivalent execution. At runtime, the component monitor M ϕ observes the relevant pieces of information in B 1 , . . . , B n and emits verdicts according to the satisfaction or violation of ϕ. The amount of information observed in the components B 1 , . . . , B n is kept minimal so as to minimize the overhead induced by the monitoring process.

Contributions. We introduce a complementary validation technique for CBS in general and BIP systems in particular. More precisely, the contributions of this paper are as follows:

1. To propose a minimal formal introduction to BIP systems providing a framework for rigorous design of CBS. 2. To extend the BIP framework by integrating an expressive RV framework previously introduced in [?].

We extend this framework for CBS by proposing a formal instrumentation technique that allows to observe the relevant parts in the behavior of a BIP system. This instrumentation technique is formally defined, proved sound and complete, and leverages the formal semantics of BIP. Given a specification, our method uniformly integrates a monitor as an additional component in a BIP system that is able to runtime check the satisfaction or violation of the specification. 3. To propose an implementation of the RV framework, RV-BIP, allowing to automatically instrument BIP systems from the description of an abstract monitor. Thanks to the code generator of BIP, the generated self-monitoring system can be directly translated into an actual C module embedded in the global system whose behavior is checked at runtime against the specification. 4. To evaluate and validate the relevance of the whole approach on a real-world application.

This paper extends a previous contribution [?] that appeared in the 9 th International Conference on Software Engineering and Formal Methods, with the following additional contributions:

to propose a more complete and improved introduction to the BIP framework; to propose a detailed and rigorous proof of the correctness of the approach proposed in this paper; to improve the presentation and editorial quality of the previous paper by (i) formalizing some concepts that remained informal in the conference version, (ii) providing more detailed explanations in each section, (iii) correcting typos, (iv) and illustrating the concepts with additional examples; to propose additional experiments on our case study; to propose a deeper study of related work.

Paper Organization. The paper is structured as follows. Section ?? introduces the preliminary concepts needed in this paper. In Section ?? we give a minimal introduction to the BIP framework. Section ?? defines an abstract RV framework for CBS described in BIP. Section ?? shows how the abstract RV framework is implemented for BIP systems. Section ?? describes RV-BIP, an implementation used to evaluate our method on a robot application. Section ?? is dedicated to related work. Section ?? raises some concluding remarks and open perspectives. Finally, to keep our RV framework for CBS intuitive, some proofs and proof-specific definitions are omitted in Section ??, complete proofs are given in Appendix ??.

Preliminaries and Notations

We introduce some preliminary concepts and notation.

Functions and partial functions. For two domains of elements E and F , we note

[E → F ] (resp. [E F ])
the set of functions (resp. partial functions) from E to F . When elements of E depend on the elements of F , we note {e ∈ E} f ∈F , where

F ⊆ F , for {e ∈ E | f ∈ F } or {e} f ∈F when clear from context. 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 follows: v/v (x) = v (x) if x ∈ X , v(x) otherwise.
A predicate over some domain E is a function in the set [E → {true, false}] where true and false are the usual Boolean constants. Given, some predicate p over some domain E and some element e ∈ E, we abbreviate p(e) = true (resp. p(e) = false) by p(e) (resp. ¬p(e)). Given some sets of functions

[X 1 → Y 1 ], . . . , [X n → Y n ],
the set of consistent merges of these functions, denoted

[X 1 → Y 1 ], . . . , [X n →
Y n ] is defined as:

[X 1 → Y 1 ], . . . , [X n → Y n ] def = f ∈ n i=1 X i → n i=1 Y i | ∀i ∈ [1, n] : x ∈ X i ⇒ f (x) ∈ Y i .
That is, the set of consistent merges is the set of functions from the union of domains ( n i=1 X i ) to the union of co-domains ( n i=1 Y i ) where only consistent data bindings are allowed.

Pattern-matching. We shall use the mechanism of pattern-matching to define some functions more concisely. We recall an intuitive definition for the sake of completeness. Evaluating the expression:

match expression with | pattern 1 → expression 1 | pattern 2 → expression 2 . . . | pattern n → expression n
consists in comparing successively expression with the patterns pattern 1, . . . , pattern n in order.

When a pattern pattern i fits expression, then the associated expression i is returned.

Sequences. Given a set of elements E, a sequence or a list of length n over E is denoted e 1 • e 2

BIP -Behavior Interaction Priority

In this section we recall the necessary concepts of the BIP framework [?]. BIP is a component-based framework for constructing systems by superposing three layers of modeling: Behavior, Interaction, and Priority.

The behavior layer consists of a set of atomic components represented by transition systems. The interaction layer models the collaboration between components. Interactions are described using sets of ports and connectors between them [?]. The priority layer is used to enforce scheduling policies applied to the interaction layer, given by a strict partial order on interactions.

Component-based Construction

BIP offers primitives and constructs for modeling and composing complex behaviors from atomic components. Atomic components are Labeled Transition Systems (LTS) extended with C functions and data. -For each transition τ ∈ T :

• g τ is a Boolean condition over X: the guard of τ ,

• f τ ∈ {x := f x (X) | x ∈ X} * : the computation step of τ , a list of statements.

For τ = (l, p, l ) ∈ T a transition of the internal LTS, l (resp. l ) is referred as the source (resp. destination) location and p is a port through which an interaction with another component can take place. Moreover, a transition τ = (l, p, l ) ∈ T in the internal LTS involves a transition in the atomic component of the form (l, p, g τ , f τ , l ) which can be executed only if the guard g τ evaluates to true, and f τ is a computation step: a set of assignments to local variables in X.

In the rest of this article, we use the dot notation to denote the elements of atomic components, e.g., B.P denotes the set of ports of the atomic component B, B.L denotes its set of locations, etc.

Example 1 (Atomic component). Figure ?? shows an example of an atomic component with a variable x, two ports p 1 and p 2 with support set {x}, and two control locations l 1 , l 2 . At location l 1 , the transition labelled by port p 1 is possible (the guard evaluates to true by default). When an interaction through p 1 takes place, a random value is assigned to the variable x through the assignment x := rand (). From the control location l 2 , the transition labelled by the port p 2 is possible, the variable x is not modified, and the value of x is printed and exported through p 2 .

Semantics of Atomic Components. The semantics of an atomic component is an LTS over configurations and ports, formally defined as follows:

Definition 3 (Semantics of Atomic Components). The semantics of the atomic component → (l, v, p), where v p is a valuation of the variables x p attached to the port p, is possible if there exists a transition (l , p[x p ], g τ , f τ , l), such that g τ (v ) = true. As a result, the valuation v of variables is modified to v = f τ (v /v p ).

(P, L, T, X, {g τ } τ ∈T , {f τ } τ ∈T ) is an LTS (P, Q, T 0 ) such that -Q = L × [X → Data] × (P ∪ {null}), -T 0 = {((l , v , p ), p(v p ), (l, v, p)) ∈ Q × P × Q | ∃τ = (l , p[x p ], l) ∈ T : g τ (v ) ∧ v = f τ (v /v p )}, where v p ∈ [x p → Data]. A configuration is a triple (l, v, p) ∈ Q where l ∈ L is a control location, v ∈ [X → Data]
Creating composite components. Assuming some available atomic components B 1 , . . . , B n , we show how to connect the components in the set {B i } i∈I with I ⊆ [1, n] using a connector.

A connector γ is used to specify possible interactions, i.e., the sets of ports that have to be jointly executed. Two types of ports (synchron, trigger) are defined, in order to specify the feasible interactions of a connector. A trigger port is active: the port can initiate an interaction without synchronizing with other ports. A trigger port is graphically represented by a triangle. A synchron port is passive: the port needs synchronization with other ports for initiating an interaction. A synchron port is graphically represented by a circle. A feasible interaction of a connector is a subset of its ports such that either it contains some trigger, or it is maximal. Figure ?? shows two connectors: Rendezvous (only the maximal interaction {s, r 1 , r 2 , r 3 , r 4 } is possible), Broadcast (all the interactions containing the trigger port s are possible). Formally, a connector is defined as follows:

Definition 4 (Connector). A connector γ is a tuple (P γ , t, G, F ), where: A communication between the atomic components of {B i } i∈I through a connector (P γ , t, G, F ) is defined using the notion of interaction:

-P γ = {p i [x i ] | p i ∈ B i .P
Definition 5 (Interaction). A set of ports a = {p j } j∈J ⊆ P γ for some J ⊆ I is an interaction of γ if one of the following conditions holds:

1. there exists j ∈ J such that p j is trigger; 2. for all j ∈ J, p j is synchron and {p j } j∈J = P γ .

An interaction a has a guard and two functions G a , F a , respectively obtained by projecting G and F on the variables of the ports involved in a. We denote by I(γ) the set of interactions of γ. Synchronization through an interaction involves two steps. First, the guard G a is evaluated, then the update function F a is applied.

Definition 6 (Composite Component). A composite component is defined from a set of available atomic components {B i } i∈I and a set of connectors Γ . The connection of the components in {B i } i∈I using the set Γ of connectors is denoted Γ ({B i } i∈I ).

Note that a composite component obtained by composition of a set of atomic components can be composed with other components in a hierarchical and incremental fashion using the same operational semantics.

Definition 7 (Semantics of Composite Components). A state q of a composite component

Γ ({B 1 , . . . , B n }), where Γ connects the B i 's for i ∈ [1, n]
, is an n-tuple q = (q 1 , . . . , q n ) where

q i = (l i , v i ) is a state of B i .
Thus, the semantics of Γ ({B 1 , . . . , B n }) is precisely defined as a transition system (Q, A, -→), where:

-Q = B 1 .Q × . . . × B n .Q, -A = ∪ γ∈Γ {a ∈ I(γ)} is the set of all possible interactions,
--→ is the least set of transitions satisfying the following rule:

∃γ ∈ Γ : γ = (P γ , t, G, F ) ∃a ∈ I(γ) G a (v(X)) ∀i ∈ I : q i p i (v i ) -→ i q i ∧ v i = F a i (v(X)) ∀i ∈ I : q i = q i (q 1 , . . . , q n ) a -→ (q 1 , . . . , q n )
where a = {p i } i∈I , X is the set of variables attached to the ports of a, v is the global valuation of variables, and F a i is the partial function derived from F restricted to the variable associated to p i .

The meaning of the above rule is the following: if there exists an interaction a such that all its ports are enabled in the current state and its guard (G a (v(X))) evaluates to true, then the interaction can be fired. When a is fired, not-involved components remain in the same state and involved components evolve according to the interaction.

Notice that several distinct interactions can be enabled at the same time, thus introducing nondeterminism in the product behavior. One can add priorities to reduce non-determinism. In this case, one of the interactions with the highest priority is chosen non-deterministically. 6Definition 8 (Priority). Let C = (Q, A, -→) be the behavior of the composite component

Γ ({B 1 , . . . , B n }).
A priority model π is a strict partial order on the set of interactions A. Given a priority model π, we abbreviate (a, a ) ∈ π by a ≺ π a or a ≺ a when clear from the context. Adding the

priority model π over Γ ({B 1 , . . . , B n }) defines a new composite component π Γ ({B 1 , . . . , B n }) noted π(C)
and whose behavior is defined by (Q, A, -→ π ), where -→ π is the least set of transitions satisfying the following rule:

q a -→ q ¬ ∃a ∈ A, ∃q ∈ Q : a ≺ a ∧ q a -→ q q a -→ π q
Start 2 Start 1 Start 2 l 0 l 3 l 0 l 3 Task 1 Task 2 l 1 l 2 l 1 l 2 TasksControlled Controller l 0 l 1 Start 1 < Fig. 3. A composite component in BIP
An interaction a is enabled in π(C) whenever a is enabled in C and a is maximal according to π among the active interactions in C.

We adapt the notion of maximal progress to BIP systems. In BIP, the maximal progress property is expressed at the level of connectors. For a given connector γ, if one interaction a ∈ I(γ) is contained in another interaction a ∈ I(γ), then the latter has a higher priority, unless there exists an explicit priority stating the contrary. Maximal progress is enforced by the BIP engine.

Definition 9 (Maximal Progress). Given a connector γ and a priority model π, ∀a, a ∈ I(γ):

(a ⊂ a ) ∧ (a ≺ a / ∈ π) ⇒ a ≺ a .
Finally, we consider systems defined as a parallel composition of components together with an initial state.

Definition 10 (System). A BIP system S is a pair (B, Init) where B is a component and

Init ∈ B 1 .L × . . . × B n .L is the initial state of B.
For the sake of simpler notation, Init designates both the initial state of the system at the syntax level and the initial state of the underlying LTS.

Example 2 (Composite component). -(l 0 , start, true, [counter:=counter+1], l 1 ): from location l 0 , the start port is enabled, the guard is true, when the transition is executed the component goes to location l 1 and the variable counter is incremented, -(l 1 , finish, true, [ ], l 0 ): from location l 1 , the finish port is enabled, the guard is true, when the transition is executed the component goes to location l 0 and no assignment is executed, -(l 1 , fail , true, [ ], l 0 ): from location l 1 , the fail port is enabled, the guard is true, when the transition is executed the component goes to location l 0 and no assignment is executed.

The two tasks have an identical model. A task is composed of a set of locations {l 0 , l 1 , l 2 , l 3 }, a set of ports {start, exec, finish, fail , reset} and a set of transitions containing:

-(l 0 , start, true, [ ], l 1 ): from location l 0 , the start port is enabled, the guard is true, when the transition is executed the component goes to location l 1 and no assignment is executed, -(l 1 , exec, true, [ ], l 2 ): from location l 1 , the exec port is enabled, the guard is true, when the transition is executed the component goes to location l 2 and no assignment is executed, -(l 2 , finish, true, [ ], l 0 ): from location l 2 , the finish port is enabled, the guard is true, when the transition is executed the component goes back to location l 0 and no assignment is executed, -(l 2 , fail , true, [ ], l 3 ): from location l 2 , the fail port is enabled, the guard is true, when the transition is executed the component goes to location l 3 and no assignment is executed, -(l 3 , reset, true, [ ], l 0 ): from location l 3 , the reset port is enabled, the guard is true, when the transition is executed the component goes back to location l 0 and no assignment is executed.

Task 1 and Task 2 must synchronize with Controller to start/finish execution or to notify execution failure.

Each Task i synchronizes with the controller using three connectors:

-({Task i .start, Controller .start}, {(Task i .start, false), Controller .start, false)}, true, [ ]), -({Task i .finish, Controller .finish}, {(Task i .finish, false), (Controller .finish, false)}, true, [ ]), -({Task i .fail , Controller .fail }, {(Task i .fail , false), (Controller .fail , false)}, true, [ ]).
For priorities, we consider that a task always has priority to start. This can be modeled easily in BIP by adding priorities between connectors: the connectors containing the port start always have more priority than other connectors, that is, all interactions involved in Start 1 and Start 2 have more priority than the interactions involved in other connectors, for example, {Task 1 .start, Controller .start} ≺ {Task 2 .start, Controller .start}.

The composite component TasksControlled in this example is composed of a set of components {Task 1 , Task 2 , Controller } and the connectors described above. The initial state is Init = (Task 1 .l 0 , Controller .l 0 , Task 2 .l 0 ), following Definition ??, the system is (TasksControlled , Init).

An RV Framework for Component-Based Systems

We adapt classical RV frameworks dedicated to monitoring of sequential monolithic programs to CBS in general, and, to BIP systems in particular. We consider B = π(Γ ({B 1 , . . . , B n })), i.e., a priority model π over a composite component Γ ({B 1 , . . . , B n }), whose runtime semantics is π(C), defined by an LTS (Q, A, -→ π ) as introduced in Definitions ?? and ??.

Specifications for Component-Based Systems

For CBS, we consider state-based specifications to express some desired behavior. We do not assume any particular specification formalism. We require the formalism to express a subset of the possible linear-time behaviors of CBS. In order to make our approach as general as possible, we only describe the events of the possible specification language. We also assume the existence of a monitor synthesis algorithm from this specification formalism (see Section ??). For this purpose, the existing solutions (e.g., [?,?,?,?,?]) provided by the research efforts in RV can be easily adapted.

We follow a classical approach where events are built over a set of atomic propositions AP . Intuitively, an atomic proposition is a Boolean expression over the states of the components (e.g., "in the component B 1 , the variable x should be positive if in the component B 2 the variable y is negative"). More formally, an event of π(C) is defined as a state formula over the atomic propositions expressed on components involved in π(C). Let AP denote the set of atomic propositions defined with the following grammar:

Atom ::= component 1 .var 1 == component 2 .var 2 | component.var == val | component.var ≥ val | component.loc == a location | component.port == a port component.var ::= x ∈ ∪ i∈[1,n] B i .X val ::= v ∈ Data a location ::= s ∈ ∪ i∈[1,n] B i .L a port ::= p ∈ ∪ i∈[1,n] B i .P
An atomic proposition consists in a comparison of the values of some variables, the current location, or the port that is on the last executed transition.

Let Σ denote the set of events defined with the following grammar:

Event ::= Event ∨ Event | Event ∧ Event | Event ⇒ Event | ¬ Event | Atom
In the remainder of this article, we suppose that all the atomic propositions appearing in the property affect its truth-value. 7 We use Prop : Σ → 2 AP for the set of atomic propositions used in an event e ∈ π(C).

More formally, Prop is defined inductively by using the following rules: For ap ∈ Prop(e), used (ap) is the list of pairs formed by the components and the variables (or locations or ports) that are used to define ap. The expression used (ap) is defined using a pattern-matching:

Prop(component 1 .var 1 == component 2 .var 2 ) def = {component 1 .var 1 == component 2 .var 2 },
used(ap) = match(ap) with | component 1 .var 1 == component 2 .var 2 → (component 1 , var 1 ) • (component 2 , var 2 ) | component.var == val → (component, var) | component.var ≥ val → (component, var) | component.loc == a location → (component, loc) | component.port == a port → (component, port)
Example 3 (Atomic propositions, events). Suppose we want to monitor the execution ordering of the tasks involved in the composite component introduced in Example ??. Note that such kind of properties is very difficult to enforce with priorities. To verify such properties, we can observe the execution of the transitions involving the start ports of the two components. The set of atomic propositions of such a property is {Task 1 .port == start, Task 2 .port == start}. The set of events is equal to the set of atomic propositions.

Moreover, we have used (Task 1 .port == start) = (Task 1 , port) and used (Task 2 .port == start) = (Task 2 , port).

Verification Monitors

A monitor is a procedure that consumes events fed by a BIP system and producing an appraisal on the sequence of events read so far. We follow a general approach in which verification monitors are deterministic finite-state machines that produce a sequence of truth-values (a sequence of verdicts) in an expressive 4- -The truth-value c (resp. ⊥ c ) denotes "currently true" (resp. "currently false") and expresses the satisfaction (resp. violation) of the specification "if the system execution stops here". -The truth-value (resp. ⊥) is a definitive verdict denoting the satisfaction (resp. violation) of the specification: the monitor can be stopped.

valued truth-domain B 4 def = {⊥, ⊥ c , c , },
Remark 1 (Other verdict domains and monitorable properties). As demonstrated in [?], several more restricted verdict domains can be derived from B 4 so as to fit a given specification language. The set of verdicts (used for monitoring) determines the so called monitorable properties (cf. [?]). Using the four-valued domain B 4 allows to monitor any linear-time specification over finite executions, as demonstrated in [?].

Using a less expressive verdict domain such as B 3 (defined in [?]) is also possible up to a restriction on the monitorable properties (cf. [?,?]). In this paper, we present the monitoring framework with the most general verdict domain B 4 and thus do not consider any restriction on the set of monitorable properties. See [?,?] for more details.

We define the notion of monitor for a specification defined relatively to a set of events Σ expressed on a composite component. Monitors are deterministic Moore (finite-state) machines emitting a verdict on each state. and Task 2 should alternate strictly, starting with Task 2 . The monitor A alt is defined by the 5-tuple

Definition 11 (Monitor

). A monitor A is a tuple (Θ A , θ A init , Σ, -→ A , B 4 , ver A ). The finite set Θ A denotes the control states and θ A init ∈ Θ A is the initial state. The complete function -→ A : Θ A × Σ → Θ A is
(Θ A alt , θ A alt init , Σ A alt , -→ A alt , B 4 , ver A alt ). A graphical representation of A alt is depicted in Fig. ??. The set of states is Θ A alt = {θ 0 , θ 1 , θ 2 }. The initial state is θ A alt init = θ 0 . The set of events is Σ A alt = {Task 1 .port == start, Task 2 .port == start} with e 1 def = Task 1 .port == start and e 2 def = Task 2 .port == start. The set of transitions is -→ A alt = {(θ 0 , e 1 , θ 2 ), (θ 0 , e 2 , θ 1 ), (θ 0 , ¬(e 1 ∨ e 2 ), θ 0 ), (θ 1 , e 1 , θ 0 ), (θ 1 , e 2 , θ 2 ), (θ 1 , ¬(e 1 ∨ e 2 ), θ 1 ), (θ 2 , true, θ 2 )}.
Only two verdicts from B 4 are needed to monitor this property: c and ⊥. The verdicts associated to states through the verdict function are as follows: ver A alt (θ 0 ) = ver A alt (θ 1 ) = c and ver A alt (θ 2 ) = ⊥, i.e., the property is "currently true" when the monitor is in states θ 0 and θ 1 and (definitely) false when A alt is in θ 2 .

In the remainder, we consider a monitor A = (Θ A , θ A init , Σ, -→ A , B 4 , ver A ).

Runs and Traces of BIP Systems

Runtime monitors observe the evolving state of the system by processing a so-called run of the system.

Intuitively, a run is the sequence of all states reached by a BIP system during its execution. However, when monitoring a given property of a system, some information related to the current state of a system can be safely discarded to evaluate the property. In this subsection, we present the notion of run of a CBS, and how, using the vocabulary of the monitored property, we can discard some information in the run. Such an abstraction of a run is called a trace.

Runs of BIP systems. Each state q ∈ Q in the LTS of a component can be seen as an environment that maps variables used in the specification over an alphabet Σ to values. In each atomic component, we introduce two variables loc and port to represent the current location and the last executed port, respectively. Then, to construct the universe of possible environments, we build the set of functions that are consistent merges (using operator introduced in Section ??) of the functions from variables to data, from the variable B i .loc

to B i .L, from the variable port to B i .P ∪ null, for each atomic component B i , i ∈ [1, n].
Definition 12 (Environments in a component). The universe of possible environments for π(C) is

Env def = ∪ i∈[1,n] B i .X → Data , B 1 .loc → (B 1 .L)], . . . , [B n .loc → (B n .L) , B 1 .port → B 1 .P ∪ {null} , . . . , B n .port → B n .P ∪ {null}
where B i .loc and B i .port are variables containing a location name and a port name for each atomic component B i , respectively. The environment defined by a state q = (q 1 , . . . , q n ), where

q i = (l i , v i , p i ) for each i ∈ [1, n], is [[q]
] ∈ Env such that:

[[q]] def = ∪ i∈[1,n] ∪ i∈[1,n] {B i .loc → l i } ∪ ∪ x i ∈B i .X {x i → v i } ∪ ∪ i∈[1,n] {B i .port → p i } .
After an interaction bringing the component in a state q, an event e is fired if the state-formula associated to e holds, noted q e, i.e., when e evaluates to true in [[q]]. Formally, q satisfies e (denoted by q e), as defined by the following rules:

q (component 1 .var 1 == component 2 .var 2 ) ⇔ [[q]](component 1 .var 1 ) == [[q]](component 2 .var 2 ), q (component.var == val) ⇔ [[q]](component.var) == val, q (component.var ≥ val) ⇔ [[q]](component.var) ≥ val, q (component.loc == a location) ⇔ [[q]](component.loc) == a location, q (component.port == a port) ⇔ [[q]](component.port) == a port,
q (e 1 ∨ e 2 ) ⇔ (q e 1 ) ∨ (q e 2 ),

q (e 1 ∧ e 2 ) ⇔ (q e 1 ) ∧ (q e 2 ),

q (e 1 ⇒ e 2 ) ⇔ (q e 1 ) ⇒ (q e 2 ), q (¬e) ⇔ ¬(q e).

Note that, after reaching a state of the LTS corresponding to the runtime behavior of a BIP component, it is always possible to determine whether an event is fired or not by checking whether the corresponding state-formula holds or not.

Some constraints on the monitors. For the monitor to properly evaluate events in states, we impose two constraints on their events and transition function, called readiness and determinism. These constraints intuitively state that the events labelling the transitions of an abstract monitor are such that exactly one transition will be fired. This condition is expressed using the Boolean conditions corresponding to the events of the automaton. The following definition formalizes these properties.

Definition 13 (Readiness and determinism of monitors). The readiness and determinism properties of a

monitor A = (Θ A , θ A init , Σ, -→ A , B 4 , ver A ) are defined as follows. For θ ∈ Θ A , let events(A, θ) = {e ∈ Σ | θ e -→}. Then ∀θ ∈ Θ A , ∀q ∈ Env : q |= e∈events(A,θ) e (readiness)
∧ ∀e 1 , e 2 ∈ events(A, θ) : e 1 = e 2 ⇒ q |= e 1 ∧ e 2 (determinism)

Readiness means that, in any state, the disjunction of Boolean conditions corresponding to the possible events evaluates to true. Determinism means that, in any state, each pairwise conjunction of Boolean conditions corresponding to the possible events evaluates to false. Readiness and determinism ensure that in a given state, exactly one transition is fired when the monitor receives any event. Thus, given a behavior of the underlying system, only one possible verdict is dictated by the monitor.8

Monitoring a run of a composite component. We present the notion of run of a composite component and how the run is monitored.

Definition 14 (Run of a composite component). A run of length m of a system (B, Init) whose runtime

semantics is π(C) = (Q, A, -→ π ) is the sequence of environments [[q 0 ]] • [[q 1 ]] • • • [[q m ]] such that: q 0 = Init,
and, ∀i ∈ [0, m -1] :

q i ∈ Q ∧ ∃a i ∈ A : q i a i -→ π q i+1 .
Example 5 (Run of TasksControlled ). Consider the following execution scenario for the composite component TasksControlled : Task 2 get executed, then Task 1 get executed and fails, then Task 2 get executed twice. The desired property (stating that the execution of Task 1 and Task 2 should alternate strictly, starting with Task 2 ) is thus violated by this execution. This execution yields the run

[[q 0 ]] • [[q 1 ]] • • • [[q 11 ]],
where:

[[q 0 ]] = {Task 1 .loc = l 0 , Task 1 .port = null} ∪ {Controller .loc = l 0 , Controller .port = null} ∪ {Task 2 .loc = l 0 , Task 2 .port = null} [[q 1 ]] = {Task 1 .loc = l 0 , Task 1 .port = null} ∪ {Controller .loc = l 1 , Controller .port = start} ∪ {Task 2 .loc = l 1 , Task 2 .port = start} [[q 2 ]] = {Task 1 .loc = l 0 , Task 1 .port = null} ∪ {Controller .loc = l 1 , Controller .port = start} ∪ {Task 2 .loc = l 2 , Task 2 .port = exec} [[q 3 ]] = {Task 1 .loc = l 0 , Task 1 .port = null} ∪ {Controller .loc = l 0 , Controller .port = finish} ∪ {Task 2 .loc = l 0 , Task 2 .port = finish} [[q 4 ]] = {Task 1 .loc = l 1 , Task 1 .port = start} ∪ {Controller .loc = l 1 , Controller .port = start} ∪ {Task 2 .loc = l 0 , Task 2 .port = finish} [[q 5 ]] = {Task 1 .loc = l 2 , Task 1 .port = exec} ∪ {Controller .loc = l 1 , Controller .port = start} ∪ {Task 2 .loc = l 0 , Task 2 .port = finish} [[q 6 ]] = {Task 1 .loc = l 3 , Task 1 .port = fail } ∪ {Controller .loc = l 0 , Controller .port = fail } ∪ {Task 2 .loc = l 0 , Task 2 .port = finish} [[q 7 ]] = {Task 1 .loc = l 3 , Task 1 .port = fail } ∪ {Controller .loc = l 1 , Controller .port = start} ∪ {Task 2 .loc = l 1 , Task 2 .port = start} [[q 8 ]] = {Task 1 .loc = l 0 , Task 1 .port = reset} ∪ {Controller .loc = l 1 , Controller .port = start} ∪ {Task 2 .loc = l 1 , Task 2 .port = start} [[q 9 ]] = {Task 1 .loc = l 0 , Task 1 .port = reset} ∪ {Controller .loc = l 1 , Controller .port = start} ∪ {Task 2 .loc = l 2 , Task 2 .port = exec} [[q 10 ]] = {Task 1 .loc = l 0 , Task 1 .port = reset} ∪ {Controller .loc = l 0 , Controller .port = finish} ∪ {Task 2 .loc = l 0 , Task 2 .port = finish} [[q 11 ]] = {Task 1 .loc = l 0 , Task 1 .port = reset} ∪ {Controller .loc = l 1 , Controller .port = start} ∪ {Task 2 .loc = l 1 , Task 2 .port = start}
Definition 15 (Monitoring a run of a system). The verdict

[[A]](q 0 • q 1 • • • q m ) stated by A for a run [[q 0 ]] • [[q 1 ]] • • • [[q m ]] is ver A (θ m ) where ∀i ∈ [0, m -1] : θ i e -→ A θ i+1
and e is the unique event9 in θ i such that q i+1 |= e, θ i ∈ Θ A and θ 0 = θ A init .

Example 6 (Monitoring a run of TasksControlled ). Monitoring the run

[[q 0 ]] • [[q 1 ]] • • • [[q 11 ]] of Exam-
ple ?? with the monitor A alt introduced in Example ??, yields a verdict for each of the prefixes of

[[q 0 ]] • [[q 1 ]] • • • [[q 11 ]]. More precisely, we have ∀i ∈ [0, 10] : [[A alt ]](q 0 • • • q i ) = c and [[A alt ]](q 0 • • • q 11 ) = ⊥.
Building a trace from a run. One of the current challenges in RV is to alleviate the performance impact on the target program. We tackle this challenge by minimizing the information sent to the monitor. Making the monitor processing the run of the target program directly would yield a prohibitive overhead. Our proposal is to send to the monitor only a relevant abstraction of the run, called a trace. Intuitively, given a run, the obtained trace is an abstraction that permits to evaluate the specification as if the run was not abstracted, filtering many irrelevant events that are guaranteed to be irrelevant for the monitor. Given Spec(Σ), a specification defined over a vocabulary of events Σ, we design an abstraction function ↓ Σ α building this minimal abstraction. We thus define a notion of informativeness of environments built from states. Intuitively, an environment ρ 1 is less informative than an environment ρ 2 if it has less variables defined, i.e., ρ 1 ρ 2 if Dom(ρ 1 ) ⊆ Dom(ρ 2 ) and ∀x ∈ Dom(ρ 1 ) : ρ 1 (x) = ρ 2 (x). When monitoring a BIP system our aim will be to instrument it so that the least informative environment is automatically built. Moreover, according to property evaluation, monitoring the instrumented system should be equivalent to monitoring the system with the global state.

Definition 16 (Abstraction function). The abstraction function

↓ Σ α : Q → Env is the function such that: ∀q ∈ Q, ∀x ∈ Dom([[q]]) : ↓ Σ α (q)(B i .x) =    [[q]](B i .x) if ∃e ∈ Σ, ∃ap ∈ Prop(e) : (B i , x) ∈ used (ap), undef otherwise.
It turns out that it might become impossible to evaluate some atomic propositions in some abstracted environment: when an abstraction function "erases" a piece of information needed to evaluate an event e, it becomes impossible to determine whether a state q satisfies e. Intuitively, the law of excluded middle does not hold with some environments. More formally:

∀q ∈ Q, ∀e ∈ Σ : ∃ap ∈ Prop(e) : (B i , x) ∈ used (ap) ∧ [[q]](B i .x) = undef ⇒ ¬(q e) ∧ ¬(q e).
However, this situation does not arise with the abstraction function defined in Definition ??. Indeed, the proposed abstraction function preserves event evaluation because it is sound and complete. Soundness states that the abstracted evaluations are the same as the concrete evaluations. Completeness states that evaluation of all specification events remains possible: abstraction does not erase the needed information from the environment. More formally, soundness and completeness are expressed by the following property.

Property 1 (Abstraction preserves event evaluation). The previous abstraction function adheres to the two following principles:

soundness: ∀e ∈ Σ, ∀q ∈ Q : ↓ Σ α (q) e ⇒ q e ∧ ↓ Σ α (q) e ⇒ q e , completeness: ∀e ∈ Σ, ∀q ∈ Q : q e ⇒↓ Σ α (q) e ∧ q e ⇒↓ Σ α (q) e .

Proof. Soundness is a straightforward consequence of the definition of the abstraction function. The proof of the completeness property is done by induction on the structure of the event.

-Induction basis. Consider an event e ∈ AP .

• Let us treat the case where e is of the form component

1 .var 1 == component 2 .var 2 . That is, used (e) = (component 1 ,var 1 ) • (component 2 ,var 2 ).
Moreover, because e ∈ Σ then for all q,

we have:

↓ Σ α (q)(component 1 .var 1 ) = [[q]](component 1 .var 1 ) and ↓ Σ α (q)(component 2 .var 2 ) = [[q]](component 2 .var 2 ) (see Definition ??). If q e, it means that [[q]](component 1 .var 1 ) == [[q]](component 2 .var 2 ), and then ↓ Σ α (q)(component 1 .var 1 ) == ↓ Σ α (q)(component 2 .var 2 ) which implies that ↓ Σ α (q) e. If q e, it means that [[q]](component 1 .var 1 ) = [[q]](component 2 .var 2 ).
Consequently, ↓ Σ α (q)(component 1 .var 1 ) =↓ Σ α (q)(component 2 .var 2 ) and then ↓ Σ α (q) e. • Let us treat the case where e is of the form component.var == val. That is, used (e) = (component,var). Moreover, because e ∈ Σ then for all q, we have: ↓ Σ α (q)(component.var) = [[q]](component.var) (see Definition ??). If q e, it means that [[q]](component.var) == val, and then ↓ Σ α (q)(component.var) == val which implies that ↓ Σ α (q) e. If q e, it means that [[q]](component.var) = val. Consequently, ↓ Σ α (q)(component.var) = val and then ↓ Σ α (q) e. • The same principle can be followed in the cases where e is of the form: component.var ≥ val, or component.loc == a location, and component.port == a port.

-Induction step. Let us consider two events e 1 , e 2 ∈ Event such that the completeness property holds.

We consider now an event e ∈ Event built on e 1 and e 2 . We distinguish several cases according to how e is built.

• Let us treat the case where e is of the form e 1 ∨ e 2 . If (q e) ⇒ (q e 1 ) ∨ (q e 2 ). As

Prop(e 1 ) ⊆ Prop(e) and Prop(e 2 ) ⊆ Prop(e), the induction hypothesis gives (↓ Σ α (q) e 1 ) ∨ (↓ Σ α (q) e 2 ) ⇒↓ Σ α (q) (e 1 ∧ e 2 ). The same principle is applied for the case where q e • The same principle can be followed in the cases where e is of the form: e 1 ∧ e 2 , e 1 ⇔ e 2 , or ¬e 1 .

Definition 17 (Trace of a composite component). The trace defined from a run [[q

0 ]] • [[q 1 ]] • • • [[q m ]] through an abstraction function ↓ Σ α is the sequence of environments defined as ↓ Σ α (q 0 ) • ↓ Σ α (q 1 ) • • • ↓ Σ α (q m ).
Example 7 (Trace of a composite component). From the run

[[q 0 ]] • [[q 1 ]] • • • [[q 11 ]] described in Example ??, through the abstraction function ↓ Σ A act α
, we obtain the trace ↓

Σ A act α (q 0 )• ↓ Σ A act α (q 1 ) • • • ↓ Σ A act α (q 11 )
where:

↓ Σ A act α (q 0 ) = {Task 1 .port = null} ∪ {Task 2 .port = null}, ↓ Σ A act α (q 1 ) = {Task 1 .port = null} ∪ {Task 2 .port = start}, ↓ Σ A act α (q 2 ) = {Task 1 .port = null} ∪ {Task 2 .port = exec}, ↓ Σ A act α (q 3 ) = {Task 1 .port = null} ∪ {Task 2 .port = finish}, ↓ Σ A act α (q 4 ) = {Task 1 .port = start} ∪ {Task 2 .port = finish}, ↓ Σ A act α (q 5 ) = {Task 1 .port = exec} ∪ {Task 2 .port = finish}, ↓ Σ A act α (q 6 ) = {Task 1 .port = fail } ∪ {Task 2 .port = finish}, ↓ Σ A act α (q 7 ) = {Task 1 .port = fail } ∪ {Task 2 .port = start}, ↓ Σ A act α (q 8 ) = {Task 1 .port = reset} ∪ {Task 2 .port = start}, ↓ Σ A act α (q 9 ) = {Task 1 .port = reset} ∪ {Task 2 .port = exec}, ↓ Σ A act α (q 10 ) = {Task 1 .port = reset} ∪ {Task 2 .port = finish}, ↓ Σ A act α (q 11 ) = {Task 1 .port = reset} ∪ {Task 2 .port = start}.
The notion of trace evaluation by a monitor directly follows from the notion of run evaluation. Moreover, the following theorem, which is a direct consequence of Property ??, states that, for runtime verification, there is no difference regarding property evaluation to process the trace instead of the run.

Theorem 1 (Trace evaluation vs run evaluation by a monitor). For A defined on Σ, the abstraction function ↓ Σ α , and a run

[[q 0 ]] • [[q 1 ]] • • • [[q m ]],
we have:

[[A]] [[q 0 ]] • [[q 1 ]] • • • [[q m ]] = [[A]] ↓ Σ α (q 0 ) • ↓ Σ α (q 1 ) • • • ↓ Σ α (q m ) .
Proof. By induction on the length of the trace and using Property ??.

In the next section, we will instrument BIP systems in such a way that, given a specification, the minimal abstraction function (information-wise) is dynamically generated.

Verifying the Runtime Behavior of BIP Systems

This section presents how we instrument and integrate an abstract monitor A = (Θ A , θ A init , Σ, -→ A , B 4 , ver A ) for some property into a BIP system Γ ({B 1 , . . . , B n }), (l 1 0 , . . . , l n 0 ) made of a composite component Γ ({B 1 , . . . , B n }), a priority model π where the initial locations of the atomic components B 1 , . . . , B n are l 1 0 , . . . , l n 0 , respectively. We propose several transformations of the initial BIP system. Our transformations result in a BIP system where the property is automatically runtime checked against the execution of the system. More precisely, the work-flow proceeds as follows (see Fig. ??): 1. From the input abstract monitor we extract the list of components and their corresponding variables used by the monitor (Section ??).

γ 1 > γ 3 , γ 4 γ 3 γ 4 γ 1 p m γ 2 p m p intern p m p m γ 2 > γ 3 , γ 4
Fig. 5. Overview of the work-flow 2. For each component B i where i ∈ [1, n], and its corresponding variables extracted from the monitor we instrument the selected components so as to observe these variables (Section ??).

3. From the monitor we generate the corresponding atomic component: the initial monitor is translated in BIP. This component can receive the state of the underlying system and then process the information to reach a verdict. Then, we add the generated component to the input composite component (Section ??).

4. Finally, we add the new connections between the instrumented atomic components and the monitor in BIP (Section ??).

Extraction of the Information Needed

The first step is to retrieve from the monitor the set of components and their corresponding variables that should be monitored. For each selected component, transitions are instrumented to observe the just needed set of variables. For a specification expressed over Σ(π(Γ ({B 1 , . . . , B n }))) and its monitor, comp(Σ ) is the subset of {B i | i ∈ [1, n]} corresponding to the set of components that should be monitored. We also define occur(Σ) to be the subset of

{B i .loc | i ∈ [1, n]} ∪ {B i .port | i ∈ [1, n]} ∪ ∪ i∈[1,n] B i .X denoting
the set of variables used in the specification. Then from occur (Σ), we sort the variables according to the component B i (where

B i ∈ comp(Σ )) that are related to: c v ∈ [1, n] → occur (Σ) such that c v (i ) is the set of variables related to component B i . Formally: comp(Σ) = {B i | ∃e ∈ Σ, ∃ap ∈ Prop(e), ∃x ∈ B i .X : (B i , x) ∈ used (ap)}
(1)

occur (Σ) = {B i .x | ∃e ∈ Σ, ∃ap ∈ Prop(e) : (B i , x) ∈ used (ap) ∧ x ∈ B i .X} (2) ∀i ∈ [1, n] : c v (i) = {B.x ∈ occur (Σ) | B = B i } (3)

Instrumentation of Atomic Components

For a composite component Γ ({B 1 , . . . , B n }), we transform each atomic component B i , i ∈ [1, n], so that B i is able to interact with the monitor, if necessary.

Definition 18 (Instrumenting atomic components). Given B = (P, L, T, X,

{g τ } τ ∈T , {f τ } τ ∈T ) such that B = B i ∈ {B 1 , . . . , B n } for some i ∈ [1, n],
we define a new atomic component

B m =    B if B / ∈ comp(Σ ) (P m , L m , T m , X m , {g τ } τ ∈T m , {f τ } τ ∈T m ) otherwise where, (P m , L m , T m , X m , {g τ } τ ∈T m , {f τ } τ ∈T m
) is defined as follows:

-

X m = X ∪ {loc | B i .loc ∈ c v (i )} ∪ {port | B i .port ∈ c v (i )}
where loc and port are initialized to l i 0 and null, respectively;

-P m = P ∪ {p m [c v (i )]}, -L m = L ∪ {l τ } τ ∈inst(T )
, where, inst(T ) is defined as follows:

inst(T ) =    T if {B i .loc, B i .port} ∩ c v (i ) = ∅ {τ ∈ T | c v (i ) ∩ var(f τ ) = ∅} otherwise where, var(f τ ) = {x ∈ X | x := f x (X) ∈ f τ };
-T m = T \ inst(T ) ∪ τ ∈inst(T ) {in(τ ), out(τ )}, where, for a given τ = (l, p, g τ , f τ , l ), we simultaneously generate in(τ ) and out(τ ) as follows:

• in(τ ) = (l, p, g τ , f in(τ ) , l τ ), where,

f in(τ ) =                f τ if B i .loc / ∈ c v (i ) ∧ B i .port / ∈ c v (i ) f τ ; [loc := "l "] if B i .loc ∈ c v (i ) ∧ B i .port / ∈ c v (i ) f τ ; [port := "p"] if B i .loc / ∈ c v (i ) ∧ B i .port ∈ c v (i ) f τ ; [loc := "l "; port := "p"] if B i .loc ∈ c v (i ) ∧ B i .port ∈ c v (i ) • out(τ ) = (l τ , p m , true, f out(τ ) , l ), where f out(τ ) = [ ].
We denote B m = Instrum(B). In X m , loc and port are variables containing a location name and a port name respectively. In P m , p m designates the fresh port created for interacting with the monitor. Finally, inst(T ) is the set of transitions that should be instrumented: we instrument atomic components whose variables are needed by the monitor. T m designates the transitions in the instrumented atomic component.

We instrument the transitions in the corresponding atomic component that are modifying a variable involved with the monitor. If the state or the port of an atomic component is needed, all transitions are instrumented.

For each transition τ ∈ inst(T ), we add a fresh new transition to interact with the monitor. Transitions are also instrumented by adding new statements to record the state and the port name, if necessary. For instance, supposing that the state should be monitored, from the transition τ 1 = (l 0 , p 1 , true, f τ 1 , l 1 ) with f τ 1 = [done := 0], we create a new state l τ 1 and the transitions in(τ 1 ) = (l 0 , p 1 , true, f in , l τ 1 ) with f in = [done := 0; loc := "l 1 "; port := "p 1 "], and out(τ 1 ) = (l τ 1 , p 1 , true, [ ], l 1 ).

Creating an Atomic Component from a Monitor

We present how an abstract monitor A is transformed into a BIP monitor M A that mimics the behavior of A. The generated BIP monitor receives events from the monitored system and processes them to produce the same verdicts as the initial abstract monitor. To do so, we expect monitors to adhere to two properties that will be used to ensure that the monitored system behave as the initial system.

Transformation of an abstract monitor into a BIP monitor. From an abstract monitor (cf. Definition ??)

given as an XML file, we construct the corresponding atomic component in BIP that interacts with the instrumented atomic components and produces verdicts following the behavior of the original monitor.

Definition 19 (Building monitors in BIP). From a monitor A = (Θ A , θ A init , Σ, -→ A , B 4 , ver A ), we define the corresponding atomic component M A = (P, L, T, X, {g τ } τ ∈T , {f τ } τ ∈T ) as an atomic component implementing its behavior:

-X = occur(Σ), -P = {p m [X], p intern [∅]}, -L = Θ A ∪ {q mi | q i ∈ Θ A }
where each q mi state is a fresh state associated to a q i , -T = T 1 ∪ T 2 , where

• T 1 = {(q i , p m , true, [ ], q mi ) | q i ∈ Θ A }, • T 2 = {(q mi , p intern , a, print(ver A (q i )), q i ) | q i a -→ A q i ∧ (q i , p m , true, [ ], q mi ) ∈ T 1 }.
We note M A = BuildMon(A) and call M A a BIP monitor. T 1 denotes the set of transitions used to interact with the composite component. T 2 is the set of transitions used to display verdicts following the behavior of the original monitor A. The set of variables of the monitor is the set of variables used in the specification (as in Section ??).

Example 9 (Transforming an abstract monitor into a BIP monitor). <VerificationMonitor> <State id="s1" initial="true"> <Transition event="e1" nextState="s1" output="currently true"/> <Transition event="not e1" nextState="s2" output="false"/> </State> <State id="s2"> <Transition event="true" nextState="s2" output="false"/> </State> </VerificationMonitor> (a) Abstract Monitor print("currently true"); print("false");

print("false"); The following corollary states that if the initial abstract monitor adheres to the readiness and determinism properties (see Definition ??), then similar properties hold on the guards of the generated monitor.

p m comp1 port p m [e 1 ] p intern p intern [not e 1 ] p intern [true] p intern s 1 s m1 s 2 s m2 p m (b) BIP Monitor
Corollary 1 (Generating a BIP monitor preserves readiness and determinism). Under the hypothesis that A adheres to readiness and determinism, the BIP monitor M A = BuildMon(A) adheres to the readiness and determinism properties in the following sense. We transpose the notion of readiness and determinism defined for abstract monitors, for l ∈ L, let guards(M A , l) = {g τ | τ = (l, , )} be the set of guards of the transitions that can be fired in location l in the BIP monitor M A . We have:

∀l ∈ L, ∀v ∈ [X → Data] : g∈guards(M A ,l) g(v) (readiness)
∧ ∀g 1 , g 2 ∈ guards(M A , l) :

g 1 = g 2 ⇒ ¬(g 1 (v) ∧ g 2 (v)) (determinism)

Connections

The next step of our transformation is to define the connectors between:

π(Γ ({B m 1 , . . . , B m n })) the composite component consisting of instrumented atomic components where for i ∈ [1, n] B m i = Instrum(B i ) (see Definition ??), already connected with a set of connectors Γ with a priority model π, and the BIP monitor M A = BuildMon(A) obtained from an abstract monitor A, (see Definition ??). This is done by the following transformation that augments the existing set of connectors Γ and the priority model π.

Definition 20 (Connections). Given M A a BIP monitor and π(Γ ({B m 1 , . . . , B m n })) a composite component obtained as described above, the monitored composite component is

π m (Γ m (B m 1 , . . . , B m n , M A )), where, -Γ m = Γ ∪ {γ 1 , γ 2 } where γ 1 = (P γ 1 , t γ 1 , true, F γ 1 ), γ 2 = (M A .p intern , t γ 2 ,
true, ∅), and,

• P γ 1 = {B i .p m [X m i ]} B i ∈comp(Σ ) ∪ {M A .p m }; • t γ 1 : P γ 1 → {true, false}, where, ∀B i ∈ comp(Σ ) t γ 1 (B i .p m ) = true and t γ 1 (M A .p m ) = false;
• F γ 1 , the update function, is the identity data transfer from the variables in the ports of the interacting components B i (i ∈ [1, n]) to the corresponding variables in the monitor port;

• the type of the port M A .p intern in the connector γ 2 is synchron (t γ 2 (M A .p intern ) = false, that is one and only one interaction is defined by this connector: γ 2 , see Definition ??);

-π m = π ∪ {(a, a ) | a ∈ ∪ γ∈Γ I(γ) ∧ a ∈ I(γ 1 ) ∪ I(γ 2 )}.
Connecting the instrumented atomic components and the BIP monitor consists in modifying the set of connectors and the priority model. Two connectors are added: γ 1 , used by the monitor to retrieve the state of the system (e.g., the values of some variables), and, γ 2 (which is internal), used by the monitor to determine the verdict and move to a state where the monitor can receive further information from the monitored system. The priority model is augmented by giving more priority to the interactions defined by γ 1 and γ 2 than those defined by Γ (illustrated in Fig. ??). Modifying the priority model ensures that, after execution of an interaction by the involved components, the monitor produces a verdict before involving other interactions.

Summary and Discussion

We end up this section by providing a summary, giving intuition about the correctness of our transformation and discussing some features about our framework. The complete proof is in Appendix ??.

Summary. We propose a 4-stage approach to introduce runtime verification for CBS. Our method directly integrates an abstract monitor in a CBS. Thanks to the BIP framework, monitoring of a specification can be taken into account at design time. Moreover, the actual system, automatically generated from the augmented BIP model, is runtime-checked. Some intuition about the correctness. The correctness proof is omitted for the sake of readability and can be found in Appendix ??. We prefer here to give some intuition. The correctness relies on the following informal arguments. Our transformations do not modify the data nor the behavior induced by the initial interactions. No deadlock is introduced because the synthesized BIP monitor is always ready to receive events from the instrumented components. Finally, the priorities introduced when connecting the instrumented components to the BIP monitor (Section ??) guarantee that the monitor always receives fresh data, i.e., the latest system state.

Remark 2 (About the initial state). In this section, we have not detailed how the monitor retrieves the initial state of the system. Actually, for each atomic component, the initial state is modified so as to add a transition labelled with the port p m , synchronized with the monitor, so as to evaluate the initial state of the system.

Our implementation, RV-BIP, instrument atomic components this way (see Section ??).

Remark 3. In the transformation proposed in this section, one monitor is generated for the whole composite component. An adaptation of this framework could consist in generating several monitors according to the underlying architecture. Synchronization between the monitors would have to be defined.

Remark 4 (Genericity and connection with other runtime verification tools). The third stage of our transformation consists in transforming an existing abstract monitor into a BIP monitor mimicking its behavior. As we indicated before, the abstract monitor can be obtained from various existing tools dedicated to monitor synthesis. Another alternative, not developed here, is to use external monitor connected to the BIP monitor using the possibility of calling external functions in BIP. Two placements of the monitor are possible according to whether the monitor executes in the same memory space as the program (inline monitoring) or not (outline monitoring). Inline monitoring is possible with a tool such as R-MOR [?] where the BIP monitor directly queries a synthesized C monitor. Outline monitoring, using potentially any RV tool, remains also possible through some form of communication initiated by some C code called by the monitor.

6 Implementation and Evaluation 6.1 RV-BIP: A tool for Runtime Verification of BIP systems RV-BIP is a Java implementation (∼ 2500 LOC) of the transformations described in Section ??, and, is part of the BIP distribution. RV-BIP takes as input a BIP system and an abstract monitor (an XML file) and then outputs a new BIP system whose behavior is monitored. RV-BIP uses the following modules (see Fig.

Case Study: a Robotic Application

We experimented RV-BIP on a robotic application modeled in BIP: Dala robot [?,?]. The Dala robot is a large and realistic interactive system. Dala is an infinite system (in terms of states and transitions) that cannot be directly model-checked.

The functional level of the Dala robot consists of a set of modules. A module is composed of a set of services corresponding to different tasks and a set of posters where the produced data is stored and exchanged between different modules. In this section, due to the lack of space, we present a simplified model of the modules with only the services related to two properties among those we runtime checked. Each service has a status variable done: value 1 means that the corresponding task has been successfully executed. A service can be triggered through the port trigger, then it executes its task by taking the transition start and finally it returns to the initial location by the transition finish when the task is done. The execution order of some services is important. In this module, InitService initializes the robot and should be successfully executed before SetSpeedService sets the speed parameter of the robot. This requirement is formalized as "ϕ 1 and ϕ 2 ", see Table ??.

Data freshness. In Dala, the modules communicate by a set of posters. Data generated by a module is written in a poster that can be accessed by another module. The behavior of the robot might depend on this data, therefore it is necessary that the data is up to date: the data read by a service of a module (called Reader ) must be fresh enough compared to the moment it has been written (by a service called Writer ). If t 1 and t 2 respectively are the moments of reading and writing actions, then the difference between t 2 and t 1 must be less than a specific duration δ, i.e., (t 2 -t 1 ) ≤ δ. In the model, the time counter is implemented by a component Clock , and the tick transition occurs every second. This requirement is formalized as "ϕ 3 and ϕ 4 ", see Table ??.

Mutual exclusion. The services in robot Dala share the same set of posters. Different services must not access and modify data in a poster at the same time. This is an important and critical property for the robot to function correctly. We enforce this property by adding a constraint: a poster allows a writer to trigger its writing process only if the poster is not occupied by any other writer. A variable concurrent is used to (¬e 1 + ¬e 3 ) * .e 2 .(¬e 1 + ¬e 3 ) * .

(¬e 1 + ¬e 2 ) * .e 3 .(¬e 1 + ¬e 2 ) * * , where,

e 1 : (Writer 1 .port == write ∧ poster .port == write ∧ clck .port == getTime) e 2 : (Writer 2 .port == write ∧ poster .port == write ∧ clck .port == getTime) e 3 : (Writer 3 .port == write ∧ poster .port == write ∧ clck .port == getTime)
represent the number of writers that are accessing a poster. This variable is increased (or decreased) by one when a writer starts (or finishes respectively) its writing process. The property is then checked by using this variable: a write can use a poster only if the value of concurrent of the poster is 0 meaning that no other writer is using the poster. This requirement is formalized as "ϕ 5 ", see Table ??.

Complex execution order. A more complex property on the execution order involves several writers: they periodically write data to posters in a specific order. We considered this property on 3 writers: Writer 1 , Writer 2 and Writer 3 . The writing order in every period must always be as follows: Writer 1 writes to a poster first, then Writer 2 can write only when Writer 1 finishes, Writer 3 can write only when Writer 2 finishes, and the same for the next periods. To do so, each writer is assigned a unique id that is passed to the poster when it starts using the poster. This id is then used to determine the last writer that used the poster.

For example, when Writer 2 wants to access a poster, it has to check whether the id stored in the poster corresponds to Writer 1 or not. This requirement is formalized as "ϕ 6 ", see Table ??.

Experiments. Table ?? reports results on checking the ordering and freshness properties of the Dala robot. the first one might have the violation of the freshness specification whereas the second always guarantees it.

Ordering violated and

In Table ??, the columns have the following meanings:

the column time-no-monitor indicates the execution time without monitoring, the column specification

shows the monitored specification the column optimized reports the execution time and the overhead obtained with the monitor that interacts only with the two components involved in the specification, and the column not-optimized reports the execution time and the overhead obtained with a monitor that observes all components of the system (even the ones that are not involved in the specification).

The results substantiate our claim that if we monitor only components involved in the specification, using the abstraction technique defined in Section ?? and implemented in Section ??, the overhead is reduced significantly.

Related Work

We propose to overview and compare work related to the approach proposed in this paper. We distinguish three kinds of related approaches:

static verification techniques (e.g., model-checking, static analysis) dedicated to component-based systems (Section ??); general-purpose runtime verification approaches dedicated to monolithic programs (Section ??); runtime verification approaches dedicated to component-based systems (Section ??).

Static/Design-time Verification of Component-Based Systems

With the growing demand of scalability and complexity for systems, it is even more important to use verification techniques to determine whether a designed system meets its requirements. Static formal verifica-tion [?,?,?] is based on mathematical techniques to prove or disprove the correctness of a design w.r.t. a given formal specification. These techniques search for input patterns which lead to violations of the desired properties and prove the correctness when such violations do not exist. Existing formal verification methods for component-based systems are based on either static analysis or on model-checking.

Approaches based on static analysis consist in computing specific invariants in order to abstract the state space. Although approaches based on static analysis are less sensitive to state explosion, they still suffer from some limitations. First these techniques are rather limited in terms of the properties they can check: they are mostly limited to safety properties and thus some interesting behavioral properties remain out of the scope of these techniques. Moreover, since these approaches rely on abstraction and over approximation of the state space, they usually yield several false positives.

Model-checking is based on an exhaustive exploration of the state space of the model obtained from the operational semantics of the specification language. For large systems, this exploration leads to a very large number of states (the well-known state explosion problem). Despite recent advances in model-checking, the state-explosion problem is far from being solved and limit the use of these methods in componentbased systems where the state space tends to become huge due to the number of possible configurations and interactions between components. Moreover, techniques based on compositional verification [?,?,?] (less sensitive to state explosion) require to over-approximate the behavior of the unknown parts of the systemas it can be the case in BIP when using external C functions.

A compositional verification method based on invariants for checking safety properties in componentbased systems is proposed in [?,?]. The method over-approximates the set of reachable states using both local invariants that characterize local constraints of atomic components and global constraints that are induced by strong synchronization between components. Although the method has been successfully applied to largescale and complex systems, the use of invariants can deal only with safety properties and might produce many false positive counter examples.

Another compositional approach is design-by-contract [?,?] that considers a property provided by a component as a contract between this component and its environment. A contract is expressed as a pair consisting of an assumption (that the environment must satisfy) and a guarantee (the property satisfied by each component). For instance [?] provides a method that searches an implementation model that satisfies a given contract. Although the experimental results are promising, it is not always possible to find an implementation model that satisfies a given property. Moreover, the composition of contracts in concurrent systems can be very expensive.

The limitations of static validation techniques led us to investigate the use of runtime verification as an alternative and complementary technique to validate CBS.

Runtime Verification of Monolithic Programs (with mathematically-proven guarantees)

Contrarily to static-verification techniques which are exhaustive, runtime verification techniques generally focus on a single execution of the system under scrutiny. While static verification techniques can produce false-positives, runtime verification techniques can miss some property violations. However, runtime verification techniques are complementary since they apply to deployed systems.

Over more than a decade, the field of runtime verification has produced many frameworks dedicated to the verification of the behavior of monolithic programs w.r.t. user-defined specifications. Many tools have been proposed as implementations of runtime verification frameworks. One of the most successful frameworks is Java-MOP (see [?] for an overview). Java-MOP can use input specifications written in many formalisms (e.g., LTL, regular expressions, context-free grammars). Java-MOP generates an AspectJ aspect that instruments the underlying program (using weaving) and embeds the (automatically generated) monitor.

Besides its generality, Java-MOP is also efficient as demonstrated by experimentation. A series of tools and Comparison with our approach. There are several noteworthy differences between our approach and existing runtime verification techniques.

Our approach differs mainly because we do not target monolithic programs but component-based systems. Moreover, related approaches rely on aspect-oriented programming (AOP). For instance, Java-MOP automatically generates the needed AspectJ aspect while RuleR expects the user to write an aspect. In all cases, existing runtime verification frameworks use AOP to instrument the system (i.e., inserting code to observe relevant events). Since the technology of AOP is not available for component-based systems, we define our own instrumentation for BIP systems. In some sense, the proposed instrumentation mimics the usual workflow adopted by most runtime verification frameworks. Indeed, we extract from the specification the relevant events and variables that need to be observed and we directly add instrumentation code at rele-vant places in the system. Dealing with BIP system allows us to define a formal definition of the performed instrumentation, contrarily to other frameworks using AspectJ. 10Compared to the existing approaches providing mathematical guarantees about their correctness, we provide mathematically proven guarantees on the correctness of our instrumentation technique. In our approach, the monitor is considered to be an input. Previously described approaches remain compatible and are complementary. Comparison with our approach Compared to previous dynamic techniques, our approach offers several advantages. First, we use the latest advances in runtime verification using an expressive 4-valued truthdomain allowing our monitor to be generated using any monitor synthesis framework. Our RV framework only uses information about the events used in the specification. Even though the monitors presented in this paper are presented as regular properties11 , the expressiveness of the BIP language confers our monitors a potential to be Turing-complete. For instance, adding internal variables to the monitor can be done with no particular difficulty. Moreover, compared to [?], our approach is not limited to monitoring component interfaces. It is often the case that components come with an abstract behavioral model, i.e., components are gray boxes instead of black boxes. Our monitoring framework supports the three kinds of approaches (black, grey, and white). Furthermore, the specifications considered for BIP systems use locations spanning over several components allowing the specification of global behaviors of the system in composition. Our approach offers several advantages compared to Dormoy et al. [?]. First, our approach is not bound to temporal logic since it only requires a monitor written as a finite-state machine. This state-machine can be then generated by several already existing tools (e.g., Java-MOP) since it uses a generic format to express monitors. Thus, existing monitor synthesis algorithms from various specification formalisms can be re-used, up to a syntactic adaptation layer. Second, the instrumentation of the initial system and the addition of the monitor is formally defined, contrarily to [?] where the process is only overviewed. Moreover, the whole approach leverages the formal semantics of BIP allowing us to provide a formal proof of the correctness of the proposed approach. All these features confers to our approach a higher-level of confidence.

Conclusion and Future Work

Conclusion. This paper introduces runtime verification as a complementary validation technique for component-based systems written in the BIP framework. Our technique is based on a general and expressive runtime verification framework with a 4-valued truth-domain. Our solution dynamically builds a minimal abstraction of the current runtime state of the system so as to lower the overhead. Generating monitors directly as BIP components confers to our approach several advantages. First, thanks to the C code generator of BIP, we are able to generate actual monitored C programs that can be directly deployed. Second, our approach remains compatible with previously proposed runtime verification frameworks in two respects.

First, thanks to the generic format of the input abstract monitor, a light adaptation layer is needed to adapt monitors generated by other existing tools. Second, using the possibility of calling external C code, our BIP monitors can use external monitors as a service to evaluate the state of the current system. Another advantage is that our approach can adapt to different level of modelling since it does not make any particular hypothesis except the ability to observe the BIP events involved in the specification. A last advantage is that, by targeting BIP systems, we can reuse several tools and research insights proposed by previous endeavors on this topic (e.g., [?,?,?]). Our approach has been implemented in RV-BIP that smoothly integrate in the existing BIP tool-set. Finally, experimental evaluations on a robotic application substantiate our claims about the effectiveness of our instrumentation and the feasibility of our approach. Some perspectives. Our aim with this article was to propose a first formal approach to runtime verification of component-based systems. Runtime verification as a field has contributed to checking the correctness of object-oriented programs. We believe that this first approach can serve as a headway towards transferring the lessons learned and the frameworks developed to the new challenges that component-based systems require. More specifically, we propose some research perspectives. A first direction is to combine the recent advances in RV that use static analysis (see e.g., [?]). In RV, using static analysis techniques may reduce the overhead induced by a monitor by disabling unnecessary runtime checks. Also related to overhead reduction, a dynamic instrumentation technique [?], enabling the monitor to remove connectors when they are not needed anymore, would reduce the overhead even more. Another possible direction is to extend the proposed framework for runtime enforcement [?]. Runtime enforcement is an extension of RV aiming at circumventing property violation and provides better confidence in system behaviors. A more practical direction is to connect RV-BIP to the various existing monitor synthesis tools available within the RV community. Finally, given the recent advances in the multi-core and the Network on Chip technologies, we plan to customize our transformations for generating distributed monitors rather than a centralized monitor. Then, using the techniques presented in [?,?], we plan to automatically generate correct and efficient distributed implementations running on distributed platforms. is a transition system (Q, γ, -→), where Q = Q 1 × . . . × Q n (with ∀i ∈ [1, n] : Q i = B i .L) and -→ is the least set of transitions satisfying the rule: ∃γ ∈ Γ : γ = (P γ , t) ∃a ∈ I(γ) ∧ a = {p i } i∈I ∧ I ⊆ [1, n] ∀i ∈ I : q i p i -→ i q i ∀i ∈ I : q i = q i (q 1 , . . . , q n ) a -→ (q 1 , . . . , q n ) Note that since data is abstracted, an interaction γ now consists of a set of ports P γ and the function t specifying the types of ports. The notion of execution (run) of composite components, in this abstracted semantics, transposes easily from Definition ?? to abstract behaviors. Moreover, in the following, to lighten notation, given a state q ∈ Q we do not make the distinction between [[q]] and q.

A.2 Preliminary Definitions and Lemmas

We recall and introduce some definitions and intermediate results on our transformations that will be used when proving our central result in Section ??.

Observational equivalence and bi-simulation. Let us recall the notion of observational equivalence of two transition systems. It is based on the usual definition of weak bisimilarity [?], where β and β-transitions are considered unobservable.

Definition 21 (Weak simulation). Given two transition systems S 1 = (Q 1 , P 1 ∪ {β}, -→ 1 ) and S 2 = (Q 2 , P 2 ∪ {β}, -→ 2 ), the system S 1 weakly simulates the system S 2 , if there is a relation R ⊆ Q 1 × Q 2 such that the two following conditions hold:

1. ∀(q, r) ∈ R, ∀a ∈ P : q a -→ A q =⇒ ∃r : (q , r ) ∈ R ∧ r

β * •a•β *
-→ B r , and 2. ∀(q, r) ∈ R : q β -→ A q =⇒ ∃r : (q , r ) ∈ R ∧ r β * -→ B r Equation 1. says that if a state q simulates a state r and if it is possible to perform a from q to end in a state q , then there exists a state r simulated by q such that it is possible to go from r to r by performing some unobservable actions, the action a, and then some unobservable actions. Equation 2. says that if a state q simulates a state r and it is possible to perform an unobservable action from q to reach a state q , then it is possible to reach a state r by a sequence of unobservable actions such that q simulates r .

In that case, we say that the relation R is a weak simulation over S 1 and S 2 or equivalently that the states of S 1 are similar to the states of S 2 . Similarly, a weak bi-simulation over S 1 and S 2 is a relation R such that R and R -1 def = {(q 2 , q 1 ) | (q 1 , q 2 ) ∈ R} are both weak simulations. In this latter case, we say that S 1 and S 2 are observationally equivalent and we write S 1 ∼ S 2 .

System stability. We define now a notion of system stability. Intuitively, a system will be unstable when the system has sent some event to the monitor and the monitor is currently processing this event. Below, we exhibit some properties of our transformed system related to stability.

Following Definition ??, the set A m of interactions of B m can be partitioned into (1) the set A of initial interactions (present in the initial composite component), (2) the set A 1 = I(B m .γ 1 ) of interactions used by initial state of the system, let q m = (q m 1 , . . . , q m n , q mon ) be its predecessor and a be the interaction leading to q m , that is q m a -→ m q m . The interaction a belongs either to A, A 1 , or A 2 (where {A, A 1 , A 2 } is the partition of the interactions of the instrumented components as defined in the paragraph system stability):

-If a ∈ A, then the state of the monitor at state q m is equal to the state of the monitor at state q m . Indeed, the interactions in I(B m .γ) consist only of the ports of the atomic components

{B i | i ∈ [1, n]}.
Since the interaction defined by I(B m .γ 2 ) has more priority than the interactions in I(B m .γ), then necessarily in the current local state q mon of the monitor, it is not possible to fire a transition with p intern (i.e., q mon M A .p intern -→ M A ). Otherwise the interaction {p intern } would be executed since the interaction defined by I(B m .γ 2 ) consists only of the port M A .p intern , such an interaction has more priority than any other existing interaction in the system, and such an interaction would be enabled because of readiness.

-If a ∈ A 1 , then a ⊆ n i=1 {B m i .p m }. Using Definition ?? with maximal progress (Definition ??) ensures that from the local states q m i , the port p m is not enabled for all i ∈ [1, n]. Hence, we have ∀i ∈ [1, n] : q m i ∈ B i .L, that is, is stable(q m ). -If a ∈ A 2 , then q mon p intern -→ M A . Thus, the fact that q mon p m -→ M A follows directly from Definition ??.

Lemma 3 (After an unstable state the system stabilizes). Given a run q 0 • q 1 • • • q s of B m such that q i a i -→ m q i+1 holds for all i ∈ [0, s -1], we have:

∀i ∈ [0, s -1] : ¬is stable(q i ) ⇒ is stable(q i+1 ) Proof. Let us consider q i = (q i 1 , . . . , q i n , q mon ) a non stable state (i.e., ¬is stable(q i )) of the run with i ∈ [0, s -1] (hence q i is not the last state12 ). Let q i+1 = (q i+1 1 , . . . , q i+1 n , q mon ) be the successor state of q i in the run. Lemma ?? guarantees that the monitor is able to perform a transition labelled by p m in q i , that is q mon p m -→ M A . Let us consider Q u = {q i j | q i j / ∈ B j .L} be the set of locally unstable states. As q i is not stable, Q u is not empty. The set of possible interactions is the set of subsets of {B m j .p m | q i j ∈ Q u } ∪ {M A .p m }. Indeed, observe that first, these interactions have more priority than the interactions in I(B m .γ), and second that the monitor is ready q mon p m -→ M A (it is not possible to execute any interaction in I(B m .γ 2 )).

Moreover, maximal progress (Definition ??) guarantees that the executed interaction is {B m j .p m | q m j ∈ Q u } ∪ {M A .p m }. In turn, Definition ?? ensures that from all local states q i+1 j , j ∈ [1, n], the port p m is not enabled. Thus, we have is stable(q i+1 ).

A.3 Observational Equivalence between the Original and Transformed BIP Models

We are now ready to state and prove our central result.

Proposition 1. The non-instrumented system is bi-similar to the instrumented system where interactions with the monitor and internal interactions of the monitor are considered to be unobservable actions, that is:

B m ∼ B.
-If is stable(q m ), then q m a -→ m r m and (r m , r) ∈ R. In this case, we can conduct the same reasoning followed for the case (ii), and consider two cases for r m . -If ¬is stable(q m ), let q m be the next state after q m (q m β -→ m q m ). Lemma ?? ensures that q m is stable (is stable(q m )). Hence, q m = (q 1 , . . . , q n , q mon ), that is q m a -→ m r m and (r m , r) ∈ R. In this case, we can conduct the same reasoning followed for the case (ii), and consider two cases for r m .

A.4 Correctness of our Approach

The correctness of our approach is supported by two arguments.

First, the instrumented system is observationally equivalent to the non-instrumented system where the actions used to monitor the system are considered unobservable (Proposition ??). It is a standard assumption in runtime verification frameworks for monolithic programs to assume that the instrumentation code does not take part in the semantics of the monitored program. Thus the behavior of a monitored monolithic program that is considered to be relevant is built by considering the original actions (present before instrumentation) to be observable, and, the behavior generated by the instrumentation code plus the code of the monitor to be unobservable. Our instrumentation thus ensures that if the initial system produces an execution, then the same execution will be produced in the instrumented system, up to the actions needed to monitor the system.

The second argument is the correctness of the verdicts produced by the monitor. This is ensured by the freshness of the data received by the monitor, and, the fact that the monitor always receives the necessary information. Indeed, if the state of the system is modified in such a way that it influences the truth-value of the monitored property, it means that at least one atomic proposition of one event in the specification has possibly changed. Then, according to the definition of the function c v, the new values of the involved elements in the specification are transmitted to the monitor. Lemma ?? and the priorities given to the interactions of the monitor ensures that the system cannot move before the monitor has finished to treat the new state and has produced a verdict.

Fig. 1 .

 1 Fig. 1. An atomic component in BIP

Fig. 2 .

 2 Fig. 2. Connectors in BIP

  Figure ?? shows an example of a composite component that consists of three atomic components (Task 1 , Task 2 , and Controller ). The Controller component is composed of a set of ports {start, finish, fail }, a set of locations L = {l 0 , l 1 }, a variable counter initialized to 0, and a set of transitions containing:

  Prop(component.var == val) def = {component.var == val}, Prop(component.var ≥ val) def = {component.var ≥ val}, Prop(component.loc == a location) def = {component.loc == a location}, Prop(component.port == a port) def = {component.port == a port}, Prop(e 1 ∨ e 2 ) def = Prop(e 1 ) ∪ Prop(e 2 ), Prop(e 1 ∧ e 2 ) def = Prop(e 1 ) ∪ Prop(e 2 ), Prop(e 1 ⇒ e 2 ) def = Prop(e 1 ) ∪ Prop(e 2 ), Prop(¬e) def = Prop(e).

  as introduced in [?] and used in[?]. B 4 consists of the possible evaluations of a sequence of events and its possible futures relatively to the specification used to generate the monitor:

  Fig. 4. The monitor A alt for the alternation of task executions

Fig. 6 .

 6 Fig. 6. Instrumentation of an atomic component

  Figure ?? illustrates the instrumentation of the atomic component depicted on the left-hand side into the instrumented component on the right-hand side.

  Figure ?? illustrates the transformation of Definition ??. The atomic component in Fig. ?? is transformed into the BIP monitor in Fig. ??.

Fig. 7 .

 7 Fig. 7. Transforming an abstract monitor into a BIP Monitor.

-

  ??): -Extraction: this module extracts the components and the corresponding variables used in the monitor. It takes as input an abstract monitor and then outputs a list of components with their corresponding variables, Atomic Transformation: this module instruments the atomic components selected from the extraction module. It takes as input the output of the Extraction module and a BIP file containing the original BIP system, -Building Monitor: this module takes as input an abstract monitor and then outputs the corresponding atomic component, -Connections: this module constructs the new composite component whose behavior is monitored. It takes as input the output from the Atomic Transformation and Building Monitor modules and then outputs a new composite component.

Fig. 8 .

 8 Fig. 8. Two services involving the ordering specification

  Ordering guaranteed correspond to the model presented in Fig. ?? where the first one might have the violation of the ordering specification whereas the second one always guarantees it. Likewise, Data freshness violated and Data freshness guaranteed correspond to the model presented in Fig. ?? where

  approaches are based on the (less efficient) paradigm of rewriting and focus on expressiveness of the specification formalism. Some of the main efforts are Eagle [?], RuleR [?,?], LogScope [?], and TraceContract [?]. Eagle handles LTL formulae and uses progression [?]. RuleR is a more general system where specifications are encoded as a set of rewrite rules. This confers RuleR the ability to handle very expressive specifications. From an abstract point of view, LogScope is a variant of RuleR internally using state-machines. Trace-Contract is an embedding of LogScope in the Scala programming language (as an internal domain-specific language). Other efforts include TraceMatches [?], JLO [?], and LARVA [?,?]. TraceMatches extends AspectJ by allowing to write regular expressions over pointcuts. JLO generates monitors from LTL formulae where events are AspectJ pointcuts. Finally, LARVA monitors different specification formalisms such as Lustre and duration calculus. LARVA translates specifications into the so called dynamic event timed automata and then uses AspectJ to weave the monitor.Runtime verification frameworks with mathematically-proven guarantees. Several runtime verification frameworks provide mathematical guarantees on their specifics. Most of the frameworks prove the correctness of their monitor-synthesis algorithms, i.e., the verdict produced by the monitor on any trace follows the semantics of the specification used to generate the monitor.Similarly, Rosu et al. [?] recently provided proofs of the mathematical correctness of their algorithms for monitoring parametric specifications. Monitoring parametric specifications involves additional algorithms to handle the data carried out in events. A different kind of guarantee is provided byBarringer et al. in RuleR [?]: they proved the correctness of a translation from LTL to RuleR specifications.

7. 3

 3 Runtime Verification of Component-Based Systems Specification and runtime verification of the behavior of CBS have received less research attention. A first series of approaches specify the behavior of components in terms of pre and post-conditions (e.g., with JML) or assertions (e.g., using Eiffel). More recently and closer to our work is the LIME specification language [?] that allows runtime monitoring of temporal properties for component interfaces. Components are black boxes and LIME specifications define how components should interact with an external application by describing a desired behavior on the calls and returns over the interface. Concurrently and independently, Dormoy et al. proposed an approach to runtime check the correct reconfiguration of components at runtime [?]. They propose to check configurations over a variant of RV-LTL where the usual notion of state is replaced by the notion of component configuration. RV-LTL is a 4-valued variant of LTL dedicated to runtime verification introduced in [?] and used in [?].

  Transition Systems. In the following, Labelled Transition System (LTS) are used to define the semantics of BIP systems. LTSs defined over an alphabet Σ is a 3-tuple(Lab, Loc, Trans) where Lab is a set of labels, Loc is a non-empty set of locations. Trans ⊆ Loc × Lab × Loc is the transition relation. A transition Monolithic/Component-based vs Centralised/Distributed Systems. As a last preliminary notion, we stress the importance of the difference between two classifications of systems. First, systems are categorized as monolithic (vs component-based) when they are designed as a single entity (resp. an association of several entities). Second, systems are categorized as centralised (vs distributed) when they execute on a single computation unit (vs multiple computation units). Consequently, we should stress that this paper does not

• • • e n

where ∀i ∈ [1, n] : e i ∈ E. When elements of a sequence are assignments, the sequence is delimited by square brackets e.g., [x 1 := expr 1 ; . . . ; x n := expr n ]. Concatenation of assignments or sequences of assignments is denoted by "; ". The empty sequence of assignments is noted [ ]. Assignments in a sequence are executed according to their order in the list (beginning with the first elements).

5

The set of all sequences over E is noted E * . We shall use regular expressions to concisely denote sets of sequences over E. A regular expression over E defines a set of sequences over E. Given two regular expressions re 1 , re 2 over E, re 1 •re 2 (resp. re 1 + re 2 ) is a regular expression and denotes the set

{s 1 • s 2 | s 1 ∈ re 1 ∧ s 2 ∈ re 2 } (resp. re 1 ∪ re 2 ).

(l, e, l ) ∈ Trans means that the LTS can move from location l to location l by consuming label e. We abbreviate (l, e, l ) ∈ Trans by l e → Trans l or by l e → l when clear from context. Moreover, l e → is a short for ∃l ∈ Loc : l s → l . target runtime verification of distributed systems (cf. [?,?]). Note also, that from a component-based system, one can generate a distributed implementation (cf. [?]) or a centralised implementation (cf. [?]) by first transforming the component-based system into an equivalent monolithic system.

  } i∈I such that ∀i ∈ I : P γ ∩ B i .P = {p i }; t ∈ [P γ → {true, false}] such that t(p) = true if p is trigger (and t(p) = false if p is synchron); -G is a Boolean expression over the set of variables ∪ i∈I x i (the guard); -F is an update function defined over the set of variables ∪ i∈I x i . P γ is the set of connected ports called the support set of γ. The ports in P γ are tagged using function t

	indicating whether they are trigger or synchron. Moreover, for each i ∈ I, x i is a set of variables associated
	to the port p i .

Table 1 .

 1 Formalization of the requirements for the Dala robot ϕ 1 : (e 1 ) * , where, e 1 : (SetSpeedService.port == trigger ∧ ProxyInterface.port == exec) ⇒ (InitService.done == 1 ) ϕ 2 : (e 1 • e 2 ) * , where, e 1 : InitService.port == finish e 2 : SetSpeedService.port == trigger ϕ 3 : (e 1 ) * , where, e 1 : (Reader .port == read ∧ poster .port == read ∧ Clock .port == getTime) ⇒ (Clock .time -poster .wrtime ≤ 2 ) ϕ 4 : (e 1 • ( + e 2 + e 2 • e 2 ) • e 3 ) * , where, e 1 : Writer .port == write e 2 : Clock .port == tick e 3 : Reader .read == read ϕ 5 : (e 1 )

* , where, e 1 : (poster .concurrent ≤ 1 ) ϕ 6 : (¬e 2 + ¬e 3 ) * .e 1 .(¬e 2 + ¬e 3 ) * .

Table 2 .

 2 Results of monitoring the requirements Execution order and Data freshness

		time-no-monitor specification	optimized	not-optimized
				time (s) ovhd (%) time (s) ovhd (%)
	Ordering violated	1.896	ϕ 1 ϕ 2	2.045 1.953	7.8 3.0	9.163 383.0 9.192 384.0
	Ordering guaranteed	1.836	ϕ 1 ϕ 2	1.984 1.889	8.0 2.8	8.900 384.0 8.896 384.0
	Data freshness violated	1.638	ϕ 3 ϕ 4	1.684 1.682	2.8 2.6	4.337 164.0 3.773 130.0
	Data freshness guaranteed	1.634	ϕ 3 ϕ 4	1.678 1.690	2.6 3.4	4.383 168.0 3.782 131.0
	Complex ordering violated	5.359	ϕ 5	5.555	3.66	6.410	19.6
	Complex ordering guaranteed	7.057	ϕ 5	7.405	4.9	8.415	19.2
	Mutual exclusion violated	5.299	ϕ 6	5.540	4.5	6.402 20.81
	Mutual exclusion guaranteed	7.024	ϕ 6	7.366	4.86	8.405 19.66

Consequently, it does not forbid to have several assignments to a variable in such sequences. In such a case, the last assignment to this variable determines the final value of the variable.

The BIP engine implementing this semantics chooses one interaction at random, when faced with several enabled interactions.

Otherwise, some simplification of the specification shall be performed beforehand. For instance, such simplification should rule out events of the form a ∨ ¬a where a ∈ Atom.

This is a reasonable and usual hypothesis in runtime verification since one expects to characterize the behavior of an implementation in a deterministic way. Moreover, these two constraints are easily and naturally ensured by a monitor generation tool using specification written in a higher-level formalism as input. Finally, note that readiness corresponds to the standard concept of completeness in automata theory.

This event is unique because of determinism (see Definition ??).

There are some approaches proposing a formal semantics of aspect-oriented programming, but these approaches work mainly on abstract models of the underlying programming language. Moreover, to the best of our knowledge, no RV framework has proposed a formalization of its instrumentation process.

Because we use as input a monitor specified as a finite-state machine.

Otherwise the lemma holds vacuously.

Acknowledgments. The authors would like to warmly thank the anonymous reviewers for their insightful remarks.

A A Proof of Correctness of the Proposed Approach

In order to prove the correctness of our approach, we proceed according to the following stages:

1. Introducing a suitable abstraction of the system. In this abstraction, some data is discarded to focus only on the behavior of the system (Section ??).

2. Introducing some intermediate definitions and lemmas (Section ??).

3. Proving that the initial system and the instrumented system are observationally equivalent by showing a weak bi-simulation between them. This is the cornerstone of the correctness of our approach in the sense that it demonstrates that our transformation preserves the initial behavior of the system up to some actions of the monitor. This result is proved in Section ??.

4. Proving that our transformation correctly transforms the initial system (Section ??), using some intermediate lemmas from previous stages.

In the following proofs, we will consider several mathematical objects in order to prove the correctness of our framework:

is obtained from B by following the procedure described in Section ??.

A.1 Abstracting Data

With the objective of simplifying the following proofs, we introduce an abstraction consisting in analyzing the behavior of the involved components without considering some of the data. This abstraction is possible as one can notice that our transformations modify the values of some newly introduced variables but preserve the values of the variables that were present in the initial system.

Recall that a state of an atomic component is defined as a 3-tuple q = (l, v, p) where l ∈ L is the control state, v ∈ [X → Data] is a valuation of the variables X of the atomic component, p ∈ P is the port labelling the last executed transition. To simplify proofs, we introduce an abstraction that consists in omitting the variables defined in the original atomic components. This abstraction is obtained by discarding some functions and guards defined in the connectors and transitions. Moreover, a state of an atomic component q = (l, v, p) for some l ∈ L, v ∈ [X → Data]) and p ∈ P reduces to the actual control state l in the abstracted semantics. Consequently, a (global) state of B is a tuple consisting of the local states of its constituent atomic components. That is, the behavior C of the composite component B = Γ ({B 1 , . . . , B n }) the monitor to observe the behavior of the system, and (3) the set A 2 = I(B m .γ 2 ) of internal interactions of the monitor to move to the next state. We have A m = A ∪ A 1 ∪ A 2 . Moreover, the pairwise intersection of A, A 1 , A 2 is empty. Observational equivalence considers that all interactions in A 1 ∪ A 2 are labelled by unobservable events, denoted by β.

Definition 22 (Stable). Given a state q m = (q m 1 , . . . , q m n , q mon ) ∈ Q m , the predicate is stable ∈ [Q m → {true, false}] is defined as follows:

A state of a composite component, consisting of an n-tuple of the state of some atomic components, is stable if each of the n states of the atomic component belongs to the uninstrumented system. That is, the constituting local states were not introduced by the transformation proposed in Definition ??.

We now introduce the notion of state stabilization. Stabilizing a state consists in either doing nothing if this state is already stable or returning the next stable state reached by the system.

Definition 23 (State stabilization). Let q m = (q m 1 , . . . , q m n , q mon ) ∈ Q m be a state, the function stable : Q m → Q is defined as follows: stable(q m ) = q, where q = (stable 1 (q m 1 ), . . . , stable n (q m n )), where the intermediate functions

are defined as follows:

otherwise, where ∃q : (q, p m , q ) ∈ B m i .T

Intermediate lemmas. We now propose some intermediate results characterizing the status of the global system w.r.t. the notion of stable states and stabilization. The first lemma is a direct consequence of the definition of the predicate is stable and the notion of stabilization.

Lemma 1. For a given state q m = (q m 1 , . . . , q m n , q mon ), we have is stable(q m ) ⇔ stable(q m ) = (q m 1 , . . . , q m n ).

The following lemma states that when the system is in an unstable state, i.e., some constituting atomic components have performed an instrumented transition, then the arriving state is such that the monitor can perform a transition labelled by p m (and thus receive an environment from the components).

Lemma 2 (When the system is not stable the monitor waits for the system). For every state q m = (q m 1 , . . . , q m n , q mon ) ∈ Q m , the following property holds

where -→ M A is the transition relation of the monitor and p m is the port used by components to communicate with the monitor (see Definition ??).

Proof. We distinguish two cases according to whether q m is the initial state of the system or not. First, if q m is the initial state of the system, then from Definition ?? we have q mon p m -→ M A . Second, if q m is not the Proof. Following Section ??, we need to exhibit a relation R between the set of states Q m of B m and the set of states Q of B. We define R def = {(q m , q) | q m ∈ B m ∧ stable(q m ) = q}. We shall prove the three next assertions to establish that R is a weak bi-simulation:

Proof of (i):

Let us suppose that q m β -→ m r m , we have two cases according to the partition of interactions proposed in Section ??:

Let q m = (q m 1 , . . . , q m n , q mon ) and r m = (r m 1 , . . . , r m n , r mon ). Because (q m , q) ∈ R, we have q = stable(q m ) = (stable 1 (q m 1 ), . . . , stable n (q m n )). We distinguish two sub-cases according to whether q m i is stable or not. • Let us suppose that q m i is a stable state, then we have stable i (q m i ) = q m i . From the local state q m i of the atomic component B i , port B m i .p m is not enabled, hence after executing an interaction consisting only of ports p m the local state q m i does not change, that is q m i = r m i and stable i (r m i ) = stable i (q m i ). • Let us suppose q m i is not a stable state, then ∃q ∈ Q m i : stable i (q m i ) = q = q m i . From the local state q m i , the port B m i .p m is enabled. Moreover, after executing the interaction β, the local state q m i becomes r m i , where r m i = stable i (q m i ) = q (because of maximal progress, see Definition ??), and r m i ∈ B i .L (see Definition ??), that is stable i (r m i ) = r m i = stable i (q m i ). Therefore, stable(r m ) = (stable 1 (q m 1 ), . . . , stable n (q m n )) = stable(q m ) = q, thus (r m , q) ∈ R. -Case β ∈ A 2 , that is β = {M A .p intern }. Hence, after executing β none of the local states

). Therefore, stable(r m ) = (stable 1 (q m 1 ), . . . , stable n (q m n )) = stable(q m ) = q, thus (r m , q) ∈ R.

Proof of (ii):

Suppose that q m a -→ m r m . Then stable(q m ) = q m , that is, is stable(q m ). Let q m = (q m 1 , . . . , q m n , q mon ) and q = (q m 1 , . . . , q m n ), from state q interaction a is possible. Let r be the next state after executing a, that is q a -→ r. We distinguish two cases according to whether r m is stable or not:

-If is stable(r m ), then r = (r m 1 , . . . , r m n ) where r m = (r m 1 , . . . , r m n , r mon ) (Definition ??). Hence, stable(r m ) = (stable 1 (r m 1 ), . . . , stable n (r m n )) = (r m 1 , . . . , r m n ) = r, that is (r m , r) ∈ R. -If ¬is stable(r m ), let s m be the next state in the run after r m , that is r m β -→ m s m . Lemma ?? ensures that s m is stable (is stable(s m )), hence the interaction β is such that β ⊆ ∪ n i=1 {B m i .p m }. As s m is stable, then stable(s m ) = (s m 1 , . . . , s m n ) (Lemma ??), where s m = (s m 1 , . . . , s m n , s mon ). Moreover, since β ⊆ ∪ n i=1 {B m i .p m }, then stable(r m ) = (s m 1 , . . . , s m n ). Definition ?? ensures that r = (s m 1 , . . . , s m n ). That is, stable(r m ) = r, thus (r m , r) ∈ R.

Proof of (iii):

Suppose that q a -→ r. Let q m = (q m 1 , . . . , q m n , q mon ), where stable(q m ) = (q 1 , . . . , q n ). We have two cases: