Antoine El-Hokayem
email: antoine.el-hokayem@univ-grenoble-alpes.fr

Yliès Falcone
email: ylies.falcone@univ-grenoble-alpes.fr

Mohamad Jaber

Modularizing Behavioral and Architectural Crosscutting Concerns in Formal Component-Based Systems Application to the Behavior Interaction Priority Framework

We define a method to modularize crosscutting concerns in Component-Based Systems (CBSs) expressed using the Behavior Interaction Priority (BIP) framework. Our method is inspired from the Aspect Oriented Programming (AOP) paradigm which was initially conceived to support the separation of concerns during the development of monolithic systems. BIP has a formal operational semantics and makes a clear separation between architecture and behavior to allow for compositional and incremental design and analysis of systems. We distinguish local from global aspects. Local aspects model concerns at the component level and are used to refine the behavior of components. Global aspects model concerns at the architecture level, and hence refine communications (synchronization and data transfer) between components. We formalize local and global aspects as well as their composition and integration into a BIP system through rigorous transformation primitives. We present AOP-BIP, a tool for Aspect-Oriented Programming of BIP systems, demonstrate its use to modularize logging, security, and fault tolerance in a network protocol, and discuss its possible use in runtime verification of CBSs.

Introduction

A component-based approach [START_REF] Basu | Rigorous componentbased system design using the BIP framework[END_REF][START_REF] Magee | Dynamic structure in software architectures[END_REF][START_REF] Szyperski | Component Software: Beyond Object-oriented Programming[END_REF] consists in building complex systems by composing components (building blocks). Such approach confers numerous advantages (e.g., productivity, incremental construction, compositionality) that facilitate dealing with the complexity in the construction phase. Component-based design is based on the separation between interaction and computation. The isolation of interaction mechanisms allows for a global treatment and analysis on interactions between components even if local computations on components are not visible (i.e., when components are "black boxes").

A typical system consists of its main logic along with tangled code that implements multiple other functionalities. Such functionalities are often seen as secondary to the system. For example, logging is not particularly related to the main logic of most systems, yet it is often scattered throughout multiple locations in the code. Logging and the main code are separate domains and represent different concerns. A concern is defined in [START_REF] Czarnecki | Beyond objects: Generative programming[END_REF] as a "domain used as a decomposition criterion for a system or another domain with that concern". Domains include logging, persistence, and system policies such as security. Concerns are often found in different parts of a system, or in some cases multiple concerns overlap one region. These are called crosscutting concerns. Aspect-Oriented Programming (AOP) [START_REF] Kiczales | Aspectoriented programming[END_REF][START_REF]The AspectJ (TM) Programming Guide[END_REF] aims at modularizing crosscutting concerns by identifying a clear role for each of them in the system, implementing each concern in a separate module, and loosely coupling each module to only a limited number of other modules. Essentially, AOP defines mechanisms to determine the locations of the concerns in the system execution by introducing joinpoints and pointcuts. Then, it determines what to do at these locations by introducing advices. Finally, it provides a mechanism to coordinate all the advices happening at a location by introducing a process called weaving.

Motivations and challenges. In Component Based Systems (CBSs), crosscutting concerns arise at the levels of components [START_REF] Duclos | Describing and using non functional aspects in component based applications[END_REF][START_REF] Lieberherr | Aspectual collaborations: Combining modules and aspects[END_REF] (building blocks) and architectures (communications). Integrating crosscutting concerns in CBSs allows users to reason about crosscutting concerns in separation, and favors correct-by-construction design. Defining an AOP paradigm for CBSs poses multiple challenges. While the execution of a sequential program can be seen as a sequence of instructions, the semantics of a CBS is generally more complex and relies on a notion of architecture imposing several constraints on their execution. As a consequence of these constraints, AOP matching, instrumentation and modifications need to be extended to account for the architecture (i.e., data transfer and rendez-vous between components). Multiple approaches [START_REF] Pessemier | A component-based and aspect-oriented model for software evolution[END_REF][START_REF] Bruneton | An open component model and its support in Java[END_REF][START_REF] Duclos | Describing and using non functional aspects in component based applications[END_REF][START_REF] Lieberherr | Aspectual collaborations: Combining modules and aspects[END_REF][START_REF] David | An aspect-oriented approach for developing self-adaptive fractal components[END_REF] have sought to apply AOP for CBSs. However they have not formalized the AOP concepts in the context of CBSs, nor have they defined formal transformations and semantics that allow us to reason about the transformed systems rigorously.

Approach overview. We formalize AOP for CBSs. We rely on a general abstraction of CBS executions as traces, AOP is then concerned with matching segments of the trace and modifying them. We identify two views for CBSs: local and global. The local view is concerned with the behavior of a component, the component is seen as a white box and its internals are inspected. The global view is concerned with the architecture of the system, i.e., the interaction between components and their interfaces, the components are seen as black boxes. We formalize our approach by extending an existing formalism of CBSs: the Behavior Interaction Priority (BIP) framework [START_REF] Basu | Rigorous componentbased system design using the BIP framework[END_REF][START_REF] Noureddine | Reduction and abstraction techniques for BIP[END_REF]. The BIP component-based framework uses formal operational semantics. BIP consists of: [START_REF] Aksit | An object-oriented language-database integration model: The composition-filters approach[END_REF] Behavior which is handled by atomic components; [START_REF] Altisen | Aspect-oriented programming for reactive systems: Larissa, a proposal in the synchronous framework[END_REF] Interaction which describes the collaboration between the atomic components; (3) Priority determines which interaction to execute out of many. Multiple formalizations for CBS exist such as BRIC [START_REF] Dihego | Aspect-oriented development of trustworthy component-based systems[END_REF], Pi-Calculus [START_REF] Milner | The pi calculus and its applications (keynote address)[END_REF], and Fractal [START_REF] Bruneton | An open component model and its support in Java[END_REF]. The choice of BIP is mainly due to compatibility. BIP models explicitly the two views [START_REF] Sifakis | A framework for component-based construction extended abstract[END_REF], behavior models the local view while interaction and priority model the global architectural view. Furthermore, BIP can also be viewed as an architecture description language (ADL) [START_REF] Magee | Dynamic structure in software architectures[END_REF], and is used for systems modeling [START_REF] Basu | Rigorous componentbased system design using the BIP framework[END_REF]. In particular, an AADL model (which is a superset of ADL [START_REF] Filali-Amine | Development of a synchronous subset of AADL[END_REF]) can be transformed into a BIP model [START_REF] Chkouri | Translating AADL into BIP -application to the verification of real-time systems[END_REF]. In addition, BIP supports a full set of tools [START_REF] Verimag | BIP Tools[END_REF] for manipulating the BIP model, source-to-source transformations, model transformations, code generation, and compositional verification [START_REF] Bensalem | D-finder 2: Towards efficient correctness of incremental design[END_REF]. We implement our approach as a model-to-model transformation tool. We transform an existing BIP model using an AOP description to a new BIP model that implements it. For each view, we define pointcuts to target transitions and interactions as joinpoints, and modify them by appending additional computation before and after their execution. Additionally, we allow advices to change the state of atomic components. As such, we are able to implement logging, authentication, congestion control and fault tolerance to a simple network protocol (Section 8.2). In Section 8.3, we show the application to runtime verification [START_REF] Falcone | Runtime verification of component-based systems in the BIP framework with formally-proved sound and complete instrumentation[END_REF][START_REF] Kiviluoma | Run-time monitoring of architecturally significant behaviors using behavioral profiles and aspects[END_REF]. Our approach can also be used for various crosscutting concerns in CBSs such as testing, runtime enforcement [START_REF] Falcone | Fully automated runtime enforcement of component-based systems with formal and sound recovery[END_REF] and monitor synthesis [START_REF] Chen | Java-MOP: A monitoring oriented programming environment for Java[END_REF]. However, we note that our approach is intended to cover a basic set of advices and not all. For example, we do not allow for a change in priorities (and thus the scheduling) between the interactions of components. We also do not allow for the disabling of interactions. These advices can be implemented by defining more transformations following our methodology.

Paper Structure. We begin by presenting the concepts of the BIP framework and AOP in Section 2 and Section 3, respectively. In Section 4, we formalize the identification and description of concerns in the context of BIP. In general, concerns are expressed by determining their locations in the system, and their behavior at the given locations. Based on the formalization of concerns, we determine the rules that govern the integration of these concerns in a BIP system. Therefore, given an initial BIP system, and a description of concerns, we transform it so as to include the desired concerns. We distinguish and define two types of aspects: Global and Local, in Sections 5 and 6, respectively. Global aspects are used to model crosscutting concerns at the architecture level and are thus useful to refine communications (synchronization and data transfer) between components. Local aspects are used to model crosscutting concerns within components and are thus particularly useful to refine the behaviors of components. Moreover, in Section 7, we define the notion of aspect container which serves as a construct for grouping aspects. We discuss weaving strategies of aspects and their integration into a BIP system. Moreover, we define a highlevel language for writing local, global aspects, and aspect containers. Our framework is fully implemented in AOP-BIP and tested on a network protocol refined to add several crosscutting concerns: logging, authentication, congestion control and fail-safe (Section 8). Furthermore, we discuss monitoring CBSs with our approach, since runtime verification is a crosscutting concern. Finally, we present related work in Section 9, then draw conclusions and present future work in Section 10. This paper revises and significantly extends a paper that appeared in the proceedings of the 14th international conference on Software Engineering and Formal Methods (SEFM 2016) [START_REF] El-Hokayem | Modularizing crosscutting concerns in component-based systems[END_REF]. The additional contributions can be summarized as follows. First, we elaborate the general overview of our approach, and explain the applicability of our approach to other formalizations of CBSs (Section 4). Second, we present the full description of local aspects (Section 6) designed to target the local view. Third, we define the strategies for weaving aspects (Section 7), by introducing containers and weaving procedures. Fourth, we extend the experimental work to include a case study on using our approach for runtime verification of CBSs (Section 8.3). Finally, we improve the presentation and readability by adding more details and examples, elaborating on the views (Section 4.2), and improving on the notation.

Behavior Interaction Priority (BIP)

Behavior Interaction Priority (BIP) [START_REF] Basu | Rigorous componentbased system design using the BIP framework[END_REF][START_REF] Noureddine | Reduction and abstraction techniques for BIP[END_REF] allows to define systems as sets of atomic components with prioritized interactions. We present components, interactions, priorities, and their composition. First, we provide definitions for the construction of BIP systems, and then illustrate them with Example 1.

We begin by describing the update function. An update function abstracts code execution, which may modify the state of the system by reading and writing to variables.

Definition 1 (Update function). An update function F over a set of variables X is a sequence of assignments x 1 := expr X1 • • • x n := expr Xn such that ∀i ∈ [1, n] : x i ∈ X, and expr Xi is an expression using variables in set X i , for i ∈ [1, n].

The set of all sequences of update functions is denoted by F. Furthermore, for F = x 1 := expr X1 • • • x n := expr Xn , we use readvar(F ) and writevar(F ) to denote variable the read and modified variables, i.e., ∪ i∈ [1,n] X i and ∪ i∈ [1,n] {x i }, respectively. Such sets can be obtained using a simple and standard syntactic analysis of the update function. Moreover, for two update functions F 1 and F 2 , we note F 1 • F 2 , update function formed by the concatenation of F 1 and F 2 (noted F 1 F 2 to lighten the notation at places).

An atomic component is the basic computation unit. It is defined by its interface (i.e., a set of ports) and behavior defined as a Labeled Transition System (LTS) extended with data. Transitions are labeled with update functions, guards, and ports. Ports define communication and synchronization points for components. A port can be associated with some variables (of the component), to exchange data with other components. Ports are said to be exported by the component as they define its interface.

Definition 2 (Port). A port p, X p is defined by an identifier p and a set of attached local variables X p (denoted by p.vars).

Definition 3 (Atomic component). An atomic component is a tuple P, L, T, X s.t.:

• P is a set of ports;

• L is a set of control locations;

• X is a set of variables such that p∈P p.vars ⊆ X;

• T = L × P × B[X] × F × L is the set of transitions, where B[X] (resp. F) is the set of boolean predicates (resp. update functions) over X.

In a transition τ = , p τ , g τ , F τ , ∈ T , (1) is the source location; [START_REF] Altisen | Aspect-oriented programming for reactive systems: Larissa, a proposal in the synchronous framework[END_REF] is the destination location; (3) p τ is the port exported by the component; (4) g τ is the guard (a boolean predicate), a boolean function over X ; (5) F τ is an update function over X . For a component B = P, L, T, X , we denote P , L, T , X , by B .locs, B .ports, B .trans, B .vars, respectively. Additionally, we denote by B the set of all atomic components. Furthermore, for a transition τ = , p, g, F, , we denote , p, g, F , by τ.src, τ.port, τ.guard , τ.func, τ.dest, respectively. We denote by readguard(g τ ) the set of variables appearing in the expression defining g τ .

The semantics of an atomic component B is defined as an LTS. A state of the LTS consists of a location and valuation v of the variables of B where a valuation is a function from the variables of the component to a set of values. First, we define how an update function modifies a valuation. For an update function F and a valuation v, executing F on v yields a new valuation v , noted v = F (v), such that v is obtained in the usual way by the successive applications of the assignments in F taken in order and where the right-hand side expressions are evaluated with the latest constructed temporary valuation. Moreover, for two valuations v and v , v /v denotes the valuation where values in v have priority over those in v.

A transition , p

[X p ], g τ , F τ , is possible to a new state , v iff B has a transition τ = , p[X p ], g τ , F τ , ∈ B .
→= { , v , p(v p ), , v | ∃τ = , p[X p ], g τ , F τ , ∈ T .trans : g τ (v) ∧ v = F τ (v p /v)};
and, X denotes the set of possible valuations of the variables in B .locs.

Furthermore, we say that a port p is enabled in a state , v , if there exists at least one transition τ from labeled by p and its guard g τ (v) holds.

Interactions serve as the glue that coordinates (i.e., synchronization and data transfer) the components through their ports. We consider B = {B 1 , . . . , B n } a set of atomic components where the semantics of

B i is S Bi = Q Bi , P Bi , → , i ∈ [1, n],
and a set of interactions γ. An interaction consists of one or more ports of different atomic components, a guard on the variables of its ports, an update function that realizes data transfer between the ports. Definition 5 (Interaction). An interaction a ∈ γ is a tuple P a , F a , G a s.t.:

• P a ⊆ B∈B (B .ports) is a set of ports including at most one port per atomic component, i.e., ∀B ∈ B : |B .ports ∩ P a | ≤ 1.

• F a is an update function executed with the interaction such that

(readvar(F a ) ∪ writevar(F a )) ⊆ pi∈Pa (p i .vars).
• g a is a boolean expression, the guard of the interaction.

For an interaction a, we denote P a , g a , F a , as a.ports, a.guard , a.func, respectively. A composite component is defined by composing atomic components using glue consisting of interactions and priorities. Definition 6 (Semantics of a composite component). The semantics of the composite component built with B and γ

(noted γ(B)) is the LTS Q, γ, → where Q = Q B1 × Q B2 × . . . × Q Bn ,
and → is the least set of transitions satisfying the following rule:

I ⊆ [1, n] a = ({p i } i∈I , g a , F a ) ∈ γ g a ({v pi } i∈I ) ∀i ∈ I : q i pi(vi) ----→ i q i ∧ v i = g i a ({v pi } i∈I ) ∀i ∈ I : q i = q i q 1 , . . . , q n a -→ q 1 , . . . , q n
where v pi is the valuation of the variables attached to port p i and F i a is the partial update function derived from F a restricted to the variables of p i .

An interaction a is enabled iff its guard g a holds and all of its ports are enabled. An enabled interaction is selected from all interactions, based on the current states of the atomic components. The BIP engine selects one of the enabled interactions and executes its update function F a , which may modify its port variables. Then, the involved atomic components (with indices in set I) execute their corresponding transitions given the new valuations v i received by the selected ports. In the following, we consider a composite component C = γ(B) with behavior Q, γ, → .

Multiple interactions can be enabled in a configuration. Priorities are used to filter the enabled interactions and reduce non-determinism.

Definition 7 (Priority).

A priority model π over C is a strict partial order on the set of interactions γ. We abbreviate a, a ∈ π by a ≺ π a . Adding π to C results in a new composite component C = π(C) which semantics is the LTS Q, γ, → π where → π is the least set of transitions satisfying the following rule:

q a -→ q ¬(∃a ∈ γ, ∃q ∈ Q : a ≺ π a ∧ q a -→ q ) q a -→ π q
Whenever according to π an interaction a ∈ γ is selected, there does not exist an enabled interaction in γ which has higher priority than a.

A composite component, obtained by the composition of a set of atomic components, can be composed with other components (composite or atomic) in a hierarchical and incremental fashion using the same operational semantics. Our method can be applied to a hierarchical system using two different approaches: (1) by flattening the system into one composite component, and (2) using scoping rules to target individual composite components. Without loss of generality, in the first approach, we flatten a hierarchical composite component to obtain a non-hierarchical one (i.e., consisting only of atomic components and simple interactions) using the method presented in [START_REF] Bozga | Source-to-source architecture transformation for performance optimization in BIP[END_REF]. The method ensures the existence of a mapping between the hierarchical to the non-hierarchical component: all transformations applied to the flattened component can be mapped to the original system. The non-hierarchical composite component resulting from the flattening is subsequently referred to as the BIP model. The BIP model is a single closed composite component, it has no ports that are exposed to an external entity. The second approach uses syntax directives to determine the scope of the transformations. A composite component is a combination of other composite components or atomic components, both behave similarly at the interactions level (i.e., they have a similar interface through ports). As such, it is possible to simply restrict the scope to a given composite component, and treat it as a global system, using scoping syntax to determine the targeted interactions at a given level in the hierarchy. In this approach, a composite component is seen as a grey box, where the interactions and interfaces of components that form it are available, and one can iterate over the sub-components as necessary. A BIP system is the instantiation of a BIP model, it defines the initial locations and variable initialization of atomic components. Definition 8 (BIP system). A BIP system is a tuple C, q 0 , where q 0 = Init, v is the initial state with Init ∈ B 1 .locs × . . . × B n .locs being the tuple of initial locations of atomic components, and v ∈ X Init is the tuple formed by the initial valuations of all variables in atomic components X Init ⊆ B∈B (B .vars).

Example 1 (BIP system). Figure 1 depicts a BIP system composed of two atomic components: Ping and Pong. The Ping component has one variable x 1 initialized to a random number and two locations IDL 1 and SND, and two ports send 1 and recv 1 . We associate the variable x 1 with both send 1 and recv 1 . Initially, the Ping and Pong components are at the IDL 1 and IDL 2 locations, respectively. From location IDL 1 , in component Ping, port send 1 is enabled, since the guard of the transition from IDL 1 to SND holds. Similarly the transition from IDL 2 to REP in Pong is possible, and recv 2 is enabled. The interaction that has both ports send 1 and recv 2 enabled, and its guard holding, is now enabled. Since no other interaction is enabled, it executes. Its update function executes the data transfer using the ports send 1 and recv 2 and their associated variables x 1 and x 2 . Then, the update function of each transition executes, generating the acknowledgment packet in Pong. Ping will move to location SND and Pong to REP. Similarly, on the next step, the acknowledgement is sent back to Ping and it generates a new number. The two interactions ensure synchronization between the two components.

IDL 1 SND [true] send1 [true] recv1 p1 := gen() Ping send 1 recv 1 x 1 IDL 2 REP [true] recv2 p2 := ack(p2) [true] send2 Pong recv 2 send 2 x 2 [true] recv2.p2 := send1.p1 [true] recv1.p1 := send2.p2
We abstract the execution of a BIP system as a BIP trace. The trace of a BIP system consists of the state changes and interactions taken.

Definition 9 (BIP trace). A BIP trace

ρ = (q 0 • a 0 • q 1 • a 1 • • • q i-1 • a i-1 • q i )
is an alternating sequence of states of S and interactions in γ; where

q k a k -→ q k+1 ∈ →, for k ∈ [0, i -1].
The trace of a BIP system consists of the state changes and interactions executed.

Example 2 (BIP Trace). Recall the system presented in Example 1 consisting in the two components Ping and Pong. The first change in the state results in the following trace:

IDL 1 , 1 , IDL 2 , 0 • {send 1 , recv 2 } • SND, 1 , REP, 2
The above trace shows the alternations of locations and valuations of the components, and the interaction that is only represented by its ports for clarity. Initially Ping is in IDL 1 and Pong is in IDL 2 , with the variables x 1 and x 2 being initialized to 1 and 0 respectively. We use a shorthand of the interaction for clarity referring only the ports, in which case it is the interaction that consists of the set {send 1 , recv 2 }. Then, we show the resulting state after executing the interaction. Ping (resp. Pong) moves to the location SND (resp. REP), and the values for x 1 and x 2 are respectively 1 and 2. The value of p 2 has been first set to 1 through the interaction, then to 2 as the result of applying ack(1) in the transition.

Aspect-Oriented Programming (AOP)

The implementation of crosscutting concerns mentioned in the introduction leads to two typical problems: scattering and tangling [START_REF] Lieberherr | Aspectual collaborations: Combining modules and aspects[END_REF]. • Tangling happens when concerns overlap in one region of the program. Consequently, enforcing one concern may affect others.

• Scattering is the dual situation of tangling. It happens when one concern is spread across different regions of the program. Scattering concerns go against encapsulation. Developers have to manually keep track of the location of a specific concern in multiple areas of the system.

In the following example, we illustrate the above two problems on an example.

Example 3 (Crosscutting concerns). Figure 2 illustrates four different: logging, caching, persistence and security policy. A class diagram describing the classes' main methods is presented, we omitted to describe their relationships for clarity. The class diagram methods are prefixed with the four concerns as flags. If a method has a concern then some code related to the logic of that concern is included in the method. For example, the method Account.withdraw has three tangled concerns: persistence, logging, and policy. Thus, the method withdraw has to include code for persistence, logging, and logic. This code enforces the policy in addition to its own main logic. The policy concern is scattered across all four classes, hence maintaining it requires one to modify all four classes when a change is needed.

The purpose of Aspect-Oriented Programming (AOP) is to localize crosscutting concerns in an aspect. An aspect is defined in [START_REF] Kiczales | An overview of aspectj[END_REF] as "a well-modularized implementation of a crosscutting concern". These concerns are separated from the main program logic and contained in separate logical units. One example of separation of concerns is achieved by AspectJ [START_REF] Kiczales | An overview of aspectj[END_REF], which is an aspect-oriented extension to the Java programming language. A joinpoint is a well-defined point in program execution where a concern needs to be handled. It acts as a reference point to coordinate the behavior of multiple concerns. A pointcut refers to a set of joinpoints and execution context information. Basic pointcuts can be composed and identified so as to increase re-usability.

Pointcuts are the syntactic elements used to select joinpoints. A pointcut specifies a function signature, a variable name, and a module that needs to be matched. Furthermore, pointcuts are able to specify dynamic execution constraints, such as a function being invoked while inside another function (e.g., cflow pointcut in AspectJ). A pointcut regulates scattering by describing the joinpoints needed to implement the concern. An advice defines the additional behavior to be executed at each specific joinpoint selected by a pointcut. An aspect serves as the modular unit that encapsulate advices, pointcuts, and additional behavior. Furthermore, aspects may introduce their own variables, methods, and fields. This is referred to as inter-type declarations. The term inter-type designates the fact that these extra objects and code are accessible in different types (based on the matching joinpoints). The main task of an AOP language implementation is to coordinate the execution of the non-aspect code with the aspect code. This coordination has to ensure a correct execution at the joinpoint of both primary and secondary concerns. This process is called weaving and can be done at compile-time, load-time, or run-time.

Listing 1: Logging concern Example 4 (Logging concern). Listing 1 implements parts of the logging concern shown in Example 3 using AspectJ. In the case of logging, the inter-type variable is a Logger object (Line 2). The pointcut expression (lines 4-9) specifies the various method invocations to be intercepted and names the pointcut log. The advice implements the logging code. It consists of code necessary to (i) capture the arguments of the method invoked using the getArgs() method on the thisJoinPoint object (ii) capture the return value of the method invoked, and (iii) pass it to the logger. The advice is set to trigger after the pointcut (line 11), in which case, it means after a method returns. Effectively, for any of the methods defined in the pointcut, the logger will log the name of the method called, its arguments and return value.

Overview and Preliminaries of Aspect-Oriented Programming for CBSs

Defining execution points for crosscutting concerns in a program implicitly relies on the programming paradigm. In the case of AspectJ, the pointcuts are described using object-oriented terminology. For example, a pointcut is defined by specifying object types, their methods (messages) with their arguments and return values, and the fields accesses of a given object. As such the crosscutting concerns are described using object-oriented terminology. To illustrate this point, consider the fact that it is not possible to intercept changes to local variables inside methods using AspectJ because of the encapsulation and data-hiding concepts that are specific to object-oriented design. Similarly, when designing AOP pointcuts for CBSs, we restrict the pointcuts to what is relevant to component-based design.

Component-Based AOP

Developing component-based systems is a process of progressively repeating the following two stages. The first stage consists in building components that follow a certain interface. The interface defines the behavior the component must implement. In this stage, a component is a white-box, its internals are exposed to the component itself. The second stage, components are composed using their interfaces to form a system (e.g. an architecture). In this stage, a component is a black-box, its internals are not visible to the system, only its interface is. As such for CBSs in general, it is important to handle crosscutting concerns that may arise in both stages. Therefore, one can distinguish two views of CBSs, the local view and the global view. The local view is concerned with the component design itself (i.e. the first stage), and the global view is concerned with the interaction of components (i.e. the second stage).

The local view and global view are independent, in the sense that components must only implement interfaces but they can do so separately. This separation effectively characterizes the joinpoints that one can reason about. In the local view, we consider the state of the component itself and actions that modify the state. In the global view, we examine the interaction between components by examining the passing of messages across the interfaces and synchronization.

Our notion of advice includes additional computation that executes before and after a given joinpoint. In the case of local advices, we include the ability to change the location of the component. The advice can require storage of additional state information. As such, intertype variables are required for both the local and global views. They need to be accessible for the advice and each of the levels separately. Once woven into the system, advices can modify the system behavior. While it is possible to modify the system arbitrarily, we define our notion of correctness. In the scope of this paper, we consider the correctness of advice application, i.e., we verify the advice has been placed correctly at the matched joinpoint.

Overview of AOP for BIP

The BIP framework is endowed with formal semantics that describes both views. Atomic components (Definition 3) describe the internals of a given component and its implementation, while the BIP model (Definition 8) formalizes the composition of atomic components and their priorities. We recall the distinction between three various notions. First, the BIP model consists of the elements needed to represent a given system. It is used to form the LTS that represents the behavior of the system. Second, the BIP system is a runtime instantiation of the model. And lastly, the BIP trace contains the elements of the model that are executed by the LTS during runtime. While the global BIP trace (Definition 9) contains all information, we consider restrictions so that we separate the internals of components from the interactions between components. Using the information from each view, we define two types of joinpoints: global and local.

Global joinpoints. In the global view, concerns are at the level of interactions. Therefore, we focus on the interface of components. This view evaluates concerns that crosscut interactions (i.e., ports, synchronization and data transfer). The components export only their ports, on which interactions are defined. Generally, each component computes its enabled ports. The interactions that have all their ports enabled and their guard evaluating to true, are said to be enabled. The system executes the enabled interaction with the highest priority. Therefore, at the interaction level, the following operations exist: interaction enablement and interaction execution. We do not consider interaction enablement, since to inspect and instrument around it requires knowledge of the internals of components. Therefore, it is not compatible with the global view. Whenever an interaction executes, three kinds of global joinpoints can be identified: (1) synchronization between different atomic components (2) one or more atomic components sending data (3) one or more atomic components receiving data. These three joinpoints are captured by the interaction: the ports define synchronization, and variables read or written define data transfer. From a BIP trace (Definition 9), one can extract the sequence of executed interactions called the global trace.

Definition 10 (Global Trace). The global trace extracted from the BIP trace ρ = (q 0 • a 0

• q 1 • • • a i-1 • q i-1 • a i-1 • q i ), noted T (ρ), is (a 0 • a 1 • • • a i-1 ).
A global joinpoint is an interaction execution moving the system from a state to another state. We suppress the state information from the BIP trace, as the atomic components are blackboxes for the global view. For the rest of the paper, we consider E to be the set of all possible interaction executions in C, q 0 with →, and fix an arbitrary BIP trace ρ. We use two sets γ and E to distinguish between the syntax representing the interactions, and the actually executed interaction, respectively.

Local joinpoints. In the local view, we focus on atomic components seen as white boxes and seek to refine their behavior. We study the state of an atomic component to locate possible points where crosscutting concerns apply. The behavior of the atomic component consists of an LTS that changes states when a transition is taken. Therefore, we consider concerns are at the level of locations, states, transitions, guards and computations on transitions. In order to study the local view, we must define first how an atomic component contributes to the global execution of the BIP system. Since in this view we see components as white boxes, we have knowledge of the full BIP system and can extract a local execution trace for a given atomic component. We fix an atomic component B k with semantics defined by the LTS

S B k = Q B k , P B k , → B k .
In order to define events local to a given atomic component, we first define the projection of the global state on a local component to extract its own state.

Definition 11 (State projection).

The projection of a global state q = q 0 , . . . q n on a local component B k is defined as

q B k = q k .
An event local to a component is defined as a triple l, v , τ, l , v . This event denotes that an atomic component has moved from the state with location l and valuations v to another state with location l and valuations v using a transition τ . Given a composite component C composed of atomic components in a set B = {B 1 , . . . , B n }, and its BIP trace ρ = (q 0 • a

0 • q 1 • a 1 • • • q i-1 • a i-1 • q i )
, we say that E i = q i , a i , q i+1 is a global event. A global event represents a global move in the BIP system from a state to another, after executing an interaction.

Definition 12 (Event projection). We project a global event E i to a local event e i in the atomic component B k by using map(E i , B k ) where:

map(E i , B k ) =                l i , v i , τ, l i+1 , v i+1 if l i , v i = q i B k ∧ l i+1 , v i+1 = q i+1 B k ∧ p = τ.port ∧ p ∈ a i .ports ∧ τ.guard (v i ) ∧ v p = F p a ({v pj } pj ∈a.ports ) ∧ v i+1 = τ.func(v p /v i ) otherwise
The map function searches within the interaction a i executing globally for any ports in the atomic component that are both enabled and included in a i . If no ports are found, then other components are involved in a and thus the global event does not concern the local component (and map returns ). Otherwise, the function map projects both the global state before and after the interaction to the local component and set τ to be the interaction that enabled the port for the interaction to execute, and takes the local component from l i , v i to l i+1 , v i+1 . For a local event e i = l i , v i , τ, l i+1 , v i+1 we denote l i , v i , l i+1 , v i+1 , l i , l i+1 , v i , v i+1 , τ by e.q, e.q , e.l, e.l , e.v, e.v , and e.τ , respectively. We then extend function map to a sequence of global events:

map(E 0 • • • E i , B k ) = map(E 0 , B k ) • • • map(E i , B k ),
where is interpreted as the neutral element of concatenation (i.e., E • = • E = E). In the sequel, we denote T k the local trace of an atomic component B k .

BIP Trace (ρ) IDL 1 , 1 , IDL 2 , 0 • {send 1 , recv 2 } • SND, 1 , REP, 2 Global Trace (T ) {send 1 , recv 2 } Local Trace (T 0 ) IDL 1 , 1 • send 1 • SND, 1
Example 5 (Traces and views). Table 1 shows traces associated with the views. We use the ports as shorthands to interactions and transitions for clarity. The BIP trace from Example 2 is presented in the first row. We recall the two atomic components B 0 = Ping and B 1 = Pong. In the second row, the global trace associated with the global view is extracted from the BIP trace, it only contains the interactions executed, in this case {send 1 , recv 2 }. From the BIP trace, we extract the following global event:

E 0 = IDL 1 , 1 , IDL 2 , 0 , {send 1 , recv 2 } , SND, 1 , REP, 2
The third row shows the local trace for the Ping component (B 0 ). It is obtained as follows:

map(E 0 , B 0 ) = IDL 1 , 1 • send 1 • SND, 1 .
From the BIP trace, we extract only elements relevant to B 0 . We know that the interaction {send 1 , recv 2 } is executed, which is associated with the transition with port send 1 in B 0 .

To handle the concerns arising at both the local and global views, we need to formally identify and select the joinpoints described for each view. We leverage the operational semantics of a BIP model to associate joinpoints, pointcuts, and advices with the original model. For the rest of the paper, we fix an arbitrary BIP-system C, q 0 where C = π(γ(B)) is the BIP model with semantics S = Q, γ, → . In Section 5 and 6 we present the AOP concepts associated with the global and local views, respectively. For each view, we define an homogeneous notion of execution points in order to define where concerns can arise (i.e., joinpoints), and then the syntax to select these points (i.e., pointcuts). We recall that joinpoints represent points in the execution of a BIP system. Given a pointcut expression pc for a given view, we use the assertion "e pc" to indicate that an element e of a (local or global) trace matches pointcut pc. We define the legal actions at these execution points (i.e., advices) and how these actions are integrated into an existing model (i.e., weaving). We allow advices to store additional state information through the creation of additional variables both at the local and global view. These additional variables constitute the inter-type variables. Furthermore for each view, we define the function select, which returns the elements of the model (syntax) that are required to instrument so that in the resulting system, whenever the assertion (e pc) holds during runtime, we execute the advice.

Applicability to other CBS Frameworks

While we use the BIP semantics for implementation, we note that our approach applies to other CBS frameworks. In general, the program execution is abstracted as an execution trace on which AOP defines its matches and changes. Given the two defined views, we require a general trace of the system that provides information about the interactions between components. Then, knowing the internals of the system, we can project the global trace to a local trace, to determine the execution of the local component. Verifying the correctness of AOP for CBS is done by analyzing the traces and ensuring that the joinpoints match the correct trace fragments, and that advices modify the traces accordingly and minimally (i.e., only when the joinpoints match). While our approach relies on the BIP semantics for the instrumentation of aspects, one could adapt it to any formal framework that defines the semantics of the behavior of a component, and the semantics of the interactions between components.

Global Aspects

Following the general requirements of the AOP approach for CBSs described in Section 4.2, we now address the concerns arising in the global view, namely the view where components are black boxes and only the interactions are visible. For this section, we consider the composite component C = π(γ(B)) as the BIP model with a BIP trace ρ.

Global Pointcuts

Since we consider only the interaction execution joinpoint, we consider criteria for matching interactions and relate them to global joinpoints. To select a set of interactions, we use constraints over their associated ports (and their variables) and the involved data transfer. For this, a global pointcut expression has three parts: the ports themselves, a set of read variables, and a set of write variables. Note that the port variables should be involved in the computation function of the interaction. In Section 5.2, we use the read and written variables to define the context information passed to the advice.

Definition 13 (Global pointcut).

A global pointcut is a 3-tuple p, v r , v w s.t.:

• p ⊆ B∈B (B .ports) is a set of ports, • v r ⊆ pi∈p (p i .vars
) is the set of read variables, and

• v w ⊆ pi∈p (p i .vars) is the set of modified variables.
We recall from Definition 10 that the global trace is a sequence of executed interactions (a 0 • a 1 • • • a i-1 ). Using the structure of an interaction (syntax only), we can match synchronization and data transfer. Synchronization is matched using ports and data transfer by syntactic analysis of variables read and written.

Definition 14 (Matching an executed interaction with a global pointcut). An executed interaction a is a joinpoint selected by a global pointcut p, v r , v w iff a p, v r , v w , where:

a p, v r , v w iff p ⊆ a.ports ∧ v r ⊆ readvar(a.func) ∧ v w ⊆ writevar(a.func).
By construction of the global trace, the executed interaction is the same interaction found in the model. As such, one can immediately match and modify the executed interactions by modifying the model directly. Matching a global pointcut consists in selecting a subset of the interactions of a composite component.

Proposition 1. ∀a ∈ E : a gpc iff a ∈ select g (C, gpc), where: select g (C, p, v r , v w ) = {a ∈ γ | p ⊆ a .ports ∧ v r ⊆ readvar(a .func) ∧ v w ⊆ writevar(a .func)}
An interaction a ∈ γ is selected by a global pointcut p, v r , v w if and only if a involves all the ports in p, and its update function reads from the variables in v r and writes to the variables in v w . The proposition states that during the execution, the interaction a is matched (i.e., a gpc)) iff the interaction a is syntactically selected (i.e., a ∈ select g (C, gpc)). Example 6 (Interactions matched by a pointcut). Figure 3a shows the interactions obtained by matching four pointcuts:

A B C D pa 1 pb 1 pb 2 pc 1 pc 2 pd 1 pd 2 x a x b x d [g0] xb := xa [g1] xd := xd + xb [g2] f2 [g3] xb := 0 a 0 a 1 a 2 a 3 (a) Matching A B C D B {v0,v1} pa 1 pb 1 pb 2 pc 1 pc 2 pd 1 pd 2 p {v0,v1} x a x b x d v 0 v 1 [g0] f0 [g1] Fbf1Fa [g2] f2 [g3] f3 a 0 a 1 a 2 a 3 (b) Weaving
1. {pa 1 , pb 1 } , ∅, ∅ selects all interactions including {pa 1 , pb 1 } in their ports, i.e., it selects only a 0 (e.g. select g (C, {pa 1 , pb 1 } , ∅, ∅ ) = a 0 ) as it is the only interaction involving both ports.

2. {pb 2 } , ∅, ∅ selects all interactions including {pb 2 } in their ports, i.e., it selects interactions a 1 and a 3 , since they both involve pb 2 .

3. {pb 2 } , {x b } , ∅ selects interactions including {pb 2 } and which computation reads variable x b associated with pb 2 . The pointcut only selects a 1 .

4. {pd 1 } , {x d } , {x d } selects interactions that include {pd 1 } and which computation read and write the variable x d associated with pd 1 (to receive data). The pointcut only selects a 1 .

Global Advice and Global Aspect

A global advice defines the possible actions allowed on a global joinpoint q, a, q . These actions are restricted to two update functions F b and F a executed respectively before and after the interaction function a.func. Moreover, a global advice can modify only the ports that it matches, as interactions could include other ports. Normally an update function of the interaction can modify the variables of all ports. The non-matching ports and their variables are hidden from the advice as per application of Demeter's law [START_REF] Lieberherr | Formulations and benefits of the law of Demeter[END_REF], as such we assume as little as possible on the interactions, and promote loose-coupling. In the rest of the section, we consider a global pointcut pc = {p 1 , . . . , p n } , v r , v w , an advice is restricted to the set of ports {p 1 , . . . , p n } and their variables, and a set of extra variables V (inter-type variables).

Definition 15 (Global advice). Given a set of ports p ⊆ B∈B B .ports and a set of inter-type variables V , X adv = V ∪ pi∈p (p i .vars) is the set of advice variables. A global advice is a pair of update functions F b , F a such that:

• (readvar(F b ) ∪ writevar(F b )) ⊆ X adv , and
• (readvar(F a ) ∪ writevar(F a )) ⊆ X adv .
The global advice bound to p and V is noted gadv(p, V ).

Functions F b and F a are referred to as the before and after advice functions, respectively. For simplicity and clarity, we assume the update functions F b and F a to be uniquely determined and not empty. To ensure this, one can add code markers at the start and end of each F b and F a which have no effect and are not present in the original system. The variables that they read and write (captured with readvar and writevar, respectively) should be variables of the advice.

We bind an advice to a pointcut expression with a global aspect. The advice then applies to every joinpoint that the pointcut matches.

Definition 16 (Global aspect).

A global aspect is a tuple C, V, gpc, gadv(p, V ) s.t.:

• C is a composite component;

• V is the set of inter-type variables associated with the aspect;

• gpc = p, v r , v w is the global pointcut (as per Definition 13);

• gadv(p, V ) is the global advice (as per Definition 15).

A global aspect therefore associates a pointcut to an advice. It ensures that the ports referred to the pointcut are the same for the advice, and that the advice has access to the variables of all ports in p and V .

Example 7 (Global advice and global aspect). The global aspect

C, {v 0 } , {pd 1 } , {x d } , {x d } , v 0 := x d , x d := v 0
defines the inter-type variable v 0 . It also defines the pointcut to match the interactions that include port pd 1 and which update function reads and writes to x d . The before and after update functions associated with the advice are respectively v 0 := x d and x d := v 0 ; saving the value of x d in v 0 before the update function executes and then setting it back afterwards. The pointcut matches a 1 as illustrated in Fig. 3a and specifies that a 1 must execute the following sequence of instructions:

(v 0 := x d ), (x d := x d + x b ), (x d := v 0
) . An advice function in this case can access only {v 0 } ∪ pd 1 .vars. The advice functions have no access to x b , as it is not related to port pd 1 but pb 2 . This aspect disallows all interactions that read and write to x d to modify its value.

Global Weaving

Using the global aspect, the weaving procedure instruments the BIP model. The procedure ensures that during the execution, the resulting BIP system will execute the advice whenever a joinpoint is reached. Recall that interactions are stateless (i.e., they have no variables of their own), but they rely on data transfer from ports. Variables can be defined only in atomic components. Therefore, the weaving procedure must create an extra atomic component (so called inter-type component) that contains the variables of the aspect along with necessary ports and interactions. The weaving operation is concerned only with syntactically modifying the BIP model. For this purpose, we separate the two notions of matching to find the locations to modify from the instrumentation itself. We therefore define first the transformation procedure and then its application with matching.

The transformation procedure uses the following input parameters:

• a BIP composite component C (the BIP model);

• a set of interactions I resulting from matching with select g (Proposition 1);

• a set of extra variables (i.e., the inter-type variables);

• the two functions F b and F a of the advice.

Accordingly, we create a new BIP composite component where the update function of each a ∈ I is preceded by F b and followed by F a . In the following, we describe the weaving of a global aspect which requires weaving of the inter-type component and weaving of the advice.

Generating an inter-type component. We first define the inter-type component.

Definition 17 (Inter-type component). The inter-type component associated to the set of intertype variables V is defined as

B V = {p V } , { 0 } , { 0 , p V , true, , 0 } , V where p V = p V , V .
B V contains V as its variables, one port p V = p V , V with all the variables attached to it, and one control location with a transition labeled with p V and guarded with the expression true. This ensures that the port will not stop any other interaction from executing once connected to it. The inter-type component is added to the set of atomic components B of the BIP model.

C = π (γ (B ∪ {B V }))
is the new composite component; with:

• B V = {p V } , { 0 } , { 0 , p V , true, , 0 } , V is the inter-type component identified by V (as per Definition 17);
• γ is defined as {m(a) | a ∈ γ} with:

m(a) : γ → γ = a.ports ∪ {p V } , F b , a.func, F a , a.guard if a ∈ I, a otherwise. • π = { m(a), m(a ) | a, a ∈ π} is the updated priority model. Weaving a global aspect GA = C, V, gpc, F b , F a into a composite component C is noted C g GA and yields a new composite component C = weave g (C, select g (C, gpc), V, F b , F a ).
The inter-type component B V is added to the model. The interactions that require instrumentation (i.e., those in γ ∩ I) are extended with the port p V so as to have access to the inter-type variables and their computation function is prepended with F b and F a . The interactions not matched (i.e., those in γ \ I) are unmodified and copied.

The priority model (π ) is only extended to the changed interactions (m(a)), but otherwise unmodified.

Example 9. Figure 3b illustrates the weaving on the set of interactions {a 1 } with the set of intertype variables V = {v 0 , v 1 } of the advice F b , F a . A new atomic component B V is created that has two local variables v 0 and v 1 and has its port p V always enabled. The variables in V are attached to p V .

• Interaction a 1 is connected to p V so as to allow access to V on which F b and F a can operate.

• Update function F b is prepended to a 1 .func so as to execute before and F a is appended to a 1 .func so as to execute after.

• Since p V is always enabled, interaction a 1 will be enabled whenever pb 2 and pd 1 are both enabled and g 1 holds. The addition of p V does not affect enablement.

• Once a 1 is executed, F b and F a can modify the inter-type variables in B V by modifying p V .vars.

Correctness of weaving. Consider E (resp. E) to be the set of executed interactions in the output (resp. initial) BIP system C , q 0 (resp. C, q 0 ), where C = C g C, V, gpc, F b , F a . We begin by defining function rem g : E × F × F → E ∪ { }. Function rem g removes the global advice from an interaction in E and constructs a similar interaction in E or the empty interaction if it does not match the advice.

rem g (a, F b , F a ) = a if ∃F : a.func = F b , F, F a , otherwise,
with: a = a.ports \ {p V } , F, a.guard , where a.func = F b , F, F a .

The following proposition expresses the correct application of the advice on the joinpoints selected by a pointcut expression.

Proposition 2 (Weaving correctness).

∀a ∈ E , ∃F : a.func = F b , F, F a iff (e = ∧ e gpc), with e = rem g (a, F b , F a ).

We say that the update function of an interaction satisfies an advice weaving if its update function (a.func) starts with F b and ends with F a (i.e., the before and after update functions). Proposition 2 states that any interaction in the execution satisfies an advice weaving iff one can construct an event e without the advice with F b and F a (e = rem g (a, F b , F a )) which matches gpc (e gpc) in the initial system. Since an advice can add extra behavior such as reading and writing to variables, it can cause the event to match more joinpoints, therefore we remove the extra update functions before matching with gpc.

| 'readVarGuard' '(' x ')' | 'readVarFunc' '(' x ')' | 'write' '(' x ')' | 'portEnabled' '(' p ')' | 'portExecute' '(' p ')'
Example 10 (Correctness of global weave). We use the example with components Ping and Pong, and its traces presented in Example 5. The global trace consists of the single interaction a = {send 1 , recv 2 } , recv 2 .p 2 := send 1 .p 1 , true . Consider the global aspect GA = C, ∅, {send 1 } , ∅, ∅ , F b , F a . GA executes the advice when an interaction with port send 1 executes. The global trace of the system after weaving consists of the interaction

a = {send 1 , recv 2 } , F b • recv 2 .p 2 := send 1 .p 1 • F a , true .
This is correct w.r.t Proposition 2: we have rem g (a , F b , F a ) = a, and a {send 1 } , ∅, ∅ holds. We note that the proposition ensures that F b and F a cannot occur in any interaction execution that does not match the pointcut. Furthermore, it is sufficient to directly edit a in the model so that the edit appears during the execution (Proposition 1).

Local Aspects

After discussing concerns that arise at the global view and following the approach discussed in Section 4.2, we now address the concerns arising in the local view. An atomic component has control locations, variables, and transitions labeled with ports, guards and computation functions. For the local view, a component B k "sees" a sequence of local events (Definition 12). A local event consists of a source state containing the location and variable valuations, a transition, and a new state. We define local joinpoints as local events, as they can be associated with the local execution of a component. We are now concerned with the matching of these joinpoints. We consider port execution and enablement, guard evaluation, access and modification of the state of the LTS (i.e., current location and valuation of local variables). → (∃q : e.q, p, q

Local Pointcuts

∈→ B k ) | portExecute(p)
→ (e.τ.port = p)

A component is considered at a location (predicate atLocation( )) if the component produces an event containing as the starting location of the transition of a local event.

Remark 1 (Location). While we can consider a component to be atLocation( ) when it produces an event containing as the ending location, we note that atLocation( ) includes evaluation of the guards and enabled ports. Therefore, we restrict atLocation( ) to select only events that start with atLocation( ) as they capture better that reasoning since that evaluation is done to decide the transition to use and the next location. As a convention, we assume that the component is at the location at the start of an event until the update function of the transition begins executing.

The evaluation of a variable x in the guard is checked on all outgoing transitions from a location regardless of the transition execution. Therefore, for readVarGuard(x), we check if any transition has x in its guard expression and originates from the location e.l. In contrast, an update function executes only when the transition is executed so we only examine the update function of e.τ , and check if a variable x is read (readVarFunc(x)) or modified (write(x)). For port enablement (portEnabled(p)), we check if there exists in the semantics of the component at least one transition labeled with the port p from the event start state to any other state. While for port execution (portExecute(p)), we only compare against e.τ as we are interested in the port that will execute.

Remark 2 (Simplification). Note that, from the semantics of BIP (Definition 6, p. 5), whenever portExecute(p) holds, then portEnabled(p) holds. Therefore, it is possible to simplify a local pointcut expression by replacing, for the same p, 'portExecute(p) and portEnabled(p)' by portExecute(p).

Matching Pointcuts

Unlike global pointcuts which map directly to interactions, local pointcuts require more complex instrumentation (i.e., location, transitions, guards, update functions). Therefore, we group the syntactic elements and define which elements precede or succeed them. This allows us to relate syntactic elements (in the BIP model) to a notion of before and after during the execution of the BIP system. 1 We use two levels of granularity. The fine (resp. coarse) granularity focuses on a given transition (resp. a group of transitions grouped by source location). We refer to a group of transitions grouped by source location as the location block . Transitions are grouped into blocks since according to the BIP semantics (Definition 4), to move from a location to another, [g5] p2 f5

[g0] p1 f0

[g1] p1 f1

[g2] p1 f2

[g3] p2 f3

[g4] p2 f4 it is necessary to evaluate all guards of all transitions originating from that location. The guard evaluation determines which ports are enabled. Each transition will then provide a jump to a location block. At the coarse level, the elements that precede a block are the blocks that have transitions linking to , while the elements that succeed are all blocks to which is a predecessor. At the fine level, the elements that syntactically precede the transition are all transitions that lead to its block. The elements that succeed the transition are all transitions in the block to which it refers to. Given a set of transitions M ⊆ B .trans, we define:

t 5 t 0 t 1 t 2 t 3 t 4 p1 p2 B x (a) BIP Model 0 t 0 : g 0 , p 1 , F 0 2 t 5 : g 5 , p 2 , F 5
1 1 t 1 : g 1 , p 1 , F 1 2 2 t 2 : g 2 , p 1 , F 2 3 t 3 : g 3 , p 2 , F 3 4 t 4 : g 4 , p 2 , F 4
• origin(M ) = {τ.src | τ ∈ M } to be the set of the origin/source locations of M (blocks that contain the transitions in M );

• dest(M ) = {τ.dest | τ ∈ M } to be the set of the destination locations of M (blocks to which the transitions lead);

• siblings(M ) = {τ ∈ B .trans | τ.src ∈ origin(M )} to be the set of transitions of B that have their source locations within the origin locations of M (selecting all transitions of the same block);

• prev(M ) = {τ ∈ B .trans | τ.dest ∈ origin(M )} to be the set of transitions of B that have their destination locations within the origin locations of M (transitions that lead to the block).

Example 11 (Syntactic representation). Figure 4 shows an atomic component in the two views. We consider the set of transitions M = {t 3 , t 5 } which is shown in bold. [g5] p2 f5

[g0] p1 f0

[g1] p1 f1

[g2] p1 f2

[g3] p2 f3

[g4] p2 f4 [g5] p2 f5

[g0] p1 f0

[g1] p1 f1

[g2] p1 f2

[g3] p2 f3

[g4] p2 f4

| atLocation( ) → {τ ∈ B k .trans | τ.src = } | readVarGuard(x) → siblings({τ ∈ B k .trans | x ∈ readguard(τ )}) | readVarFunc(x) → {τ ∈ B k .trans | x ∈ readvar(τ )} | write(x) → {τ ∈ B k .trans | x ∈ writevar(τ )} | portExecute(p) → {τ ∈ B k .trans | τ.port = p} | portEnabled(p) → siblings({τ ∈ B k .trans | τ.port = p}) | φ and φ → select (B k , φ) ∩ select (B k , φ )
Predicate atLocation( ) matches the transitions in block . Guards are evaluated at the level of the block. Therefore, to match readVarGuard(x), we first select the transitions that contain x in their guard, and then select their blocks with siblings(). An update function, however, is at the level of transitions. Henceforth, readVarFunc(x) and write(x) select only the transitions which update function reads x and modifies x, respectively. For ports, the execution of a port is at the level of a transition, therefore portExecute(p) selects all transitions that contain the port p. However, the enablement of a port happens at the level of the block, since multiple ports can be enabled but only one executes, therefore portEnabled(p) extends the selection to the block of the transitions that would normally be selected by portExecute(p). When combining matches, the result must select transitions that are affected by both pointcuts. For this, the transitions from both matches are intersected to ensure that the result has transitions present in both. Note that since ∩ is associative and commutative, the set of obtained transitions is insensitive to the match order.

Example 12 (Matching ports). Figure 5a shows (in red) the transitions matched with the pointcut portExecute(p 1 ). To match the execution of port p 1 , all transitions labeled with p 1 are selected. These transitions are executed only if port p 1 is executed. Figure 5b shows the transitions 21 matched with portEnabled(p 1 ). Note that more transitions are selected since the enablement of p 1 may be followed by the execution of a port different than p 1 (e.g., p 2 ). Port p 1 is enabled at 2 iff g 2 evaluates to true. Determining if p 1 is enabled requires pre-evaluating g 2 . Additionally, p 2 may be executed while p 1 is enabled at 2 . Then, the component may execute either t 3 or t 4 . Therefore, the joinpoint must include t 3 and t 4 . However, if g 2 evaluates to false, p 1 is not enabled. Thus the joinpoint must not include t 3 and t 4 . To handle the evaluation of the guards at runtime and executing the advice properly, additional elements need to be instrumented, they are detailed in Section 6.4. Figure 5c shows the combination of the matches from the two, effectively showing portExecute(p 1 ) since the execution implies enablement.

Proposition 3. e lpc iff e.τ ∈ select (B k , lpc) where e is a local event, and we assume that lpc does not contain portEnabled(p).

This proposition states that a local event e is a local joinpoint (e lpc) iff its transition e.τ is syntactically selected (i.e. τ ∈ select (B k , lpc)). Since state information is accessible only at runtime, determining enabled ports (portEnabled(p)) requires additional instrumentation.

Local Advice

The local advice defines the possible actions to be injected at a local joinpoint. Similarly to a global advice (Definition 15), a local advice executes two functions before and after the local joinpoint. Moreover, we introduce a constraint to restrict the variables accessible to the advice functions. Advice variables consists of the variables of the atomic component and an extra set of inter-type variables V . Furthermore, in order to increase the expressiveness of the local advice and the refinement of local behavior, a local advice may change the location of the atomic component depending on a specific guard. However to ensure consistency, the location change happens once both functions of the advice have finished executing. 2. an after function F a such that (readvar(F a ) ∪ writevar(F b )) ⊆ X adv ; 3. and a set R of reset locations, defined as a set of tuples , g where each tuple indicates that, after the end of the joinpoint, the component has to move to location if guard g evaluates to true.

Definition 21 (Local advice).

A local aspect binds a local pointcut to a local advice and defines the inter-type variables.

Definition 22 (Local aspect).

A local aspect is a tuple B k , lpc, V, ladv(B k , V ) where B k is an atomic component, lpc is a pointcut expression, V is the set of inter-type variables, ladv(B k , V ) is the local advice to apply on the joinpoints.

Example 13 (Local aspect). Let us consider the local aspect:

B k , atLocation( 2 ), {v 0 } , F b , F a , { 1 , x > 1 }
It applies to component B k . The local pointcut atLocation( 2 ) selects any joinpoint where B k is at location 2 . The advice F b , F a , { 1 , x > 1 } specifies that i) right before B k enters 2 , F b must execute, and ii) after B k exits 2 , F a must execute, and then iii) if x > 1 holds at runtime the component must move to location 1 . 22

Local Weaving

Similarly to global weaving (discussed in Section 5.3), the local weaving procedure instruments a BIP system around an atomic component. It therefore weaves a local advice to local joinpoints selected by local pointcut expressions.

Edit frame.. We recall that a local advice (see Definition 21) defines extra update functions to execute, and the possibility to change the location of the atomic component. In order to match local joinpoints with local pointcuts, we need to instrument the atomic component while using the transition as the unit (Definition 20). Then, we need to define where the instrumentation occurs relative to the transition. Using the syntactic representation in Section 6.2, we define edit points. Edit points provides hints to the weaving procedure to determine which elements need to be modified, so that during runtime, the advice executes appropriately. We identify four edit points:

• RUN (Runtime) specifies that instrumentation is to detect the state at runtime, and it applies at the block-level of the match (i.e., the location block of each transition in the match);

• PE (Previous End) specifies that the instrumentation applies at the level of the transitions that lead to the location blocks that include the match and specifically at the end of their update function;

• CB (Current Begin) specifies that the instrumentation applies at the level of the transitions in the match, at the beginning of their update function;

• CE (Current End) specifies that the instrumentation applies similarly to CB but instead, at the end of the update function.

The set of edit points is EP = {PE , CB , CE , RUN }. The edit point RUN is a special hint that is associated with runtime information. We use it to determine if a port is enabled as it requires the evaluation of the guards during runtime. We use it to encode an "if else" statement, so that the guards are evaluated in a temporary state. The temporary state is needed as advices have an update function for "before", and since we cannot wait for the evaluation to happen to execute the advice, we have to pre-evaluate the guards to determine if a port is enabled.

The edit frame indicates the start and end edit points, it informally determines the start and end of the region necessary to match the pointcut, so that we can weave F b and F a respectively. An edit frame is determined depending on the local pointcut expression as follows:

Definition 23 (Edit frame). The edit frame is a pair of edit points e 1 , e 2 corresponding to the update functions of the local advice: F b and F a respectively. It is defined as: edit(lpc) = match lpc with:

| atLocation( ) → PE , CB | readVarFunc(x) → CB , CE | readVarGuard(x) → PE , CB | write(x) → CB , CE | portEnabled(p) → RUN , CB | portExecute(p) → CB , CE | φ and φ → max(e 1 , e 1 ), max(e 2 , e 2 )
where e 1 , e 2 = edit(φ) and e 1 , e 2 = edit(φ ), with the strict ordering PE ≺ CB ≺ CE ≺ RUN .

An extra update function in the case of a location (atLocation( )) happens at the end of any transition that leads to the block . This ensures that it executes prior to the block . We consider the end of the block whenever a transition is to execute, i.e., at the beginning of its update function. This is done similarly for guards (readVarGuard(x)) as guards are evaluated at the block level. In the case of an update function F , any extra update function applies before F at its beginning, and after F at its end. Therefore, for a variable read (readVarFunc(x)) or modification (write(x)) any extra update function should happen before F . We note that this is the finest level of granularity, we do not inspect the sequence of assignments in the update function, only its beginning and end. Similarly, a port execution (portExecute(p)) is the execution of an update function of a transition so the edit points are identical. Since state information is accessible only at runtime, determining enabled ports (portEnabled(p)) requires modification at the block level, mostly by inserting additional blocks that pre-evaluate the guards and do some extra computation. Thus, we associate the edit frame RUN , CB to portEnabled so that guards are pre-evaluated appropriately.

In the case of a combination of pointcuts, we must ensure that the frame can capture both pointcuts. Thus, we define a strict order on EP : PE ≺ CB ≺ CE ≺ RUN . The purpose of the order is to select the most relevant elements for weaving, considering our representation of the syntax of BIP (described in Section 6.2). It can be seen as the scope of elements that need to be instrumented. Since RUN requires runtime checks, it always requires the most modification, therefore it is the maximal element. At the level of transitions, the order follows from the precedence: the start of an update function (CB ) precedes its end (CE ), and the entire transition is preceded by another transition that leads to its block (PE ). At the level of the block, the transitions that lead to the block, precede it (PE ). A combination of two frames must start when the elements overlap (i.e., the most delayed edit frame), and end once both end (i.e., at the most delayed one). Also, the combination must include all elements that needs to be instrumented to match both frames. To fulfill both of these conditions, we use max, as it will include the hint to the maximal elements needed to be instrumented. RUN includes the instrumentation necessary at the entire block level for detecting portEnabled at runtime. Therefore, combining RUN with any pointcut frame will still require runtime information. Therefore, RUN is defined as the maximum. Combining port enabled with the other frames adds the port enablement condition on the existing condition (as per the semantics of portEnabled in Definition 19), therefore to capture the two cases: PB , CB and CB , CE , we discriminate using the second point. When used alone, we consider portEnabled to end similarly to atLocation and readVarGuard, at the start of transition execution.

Note that, since max is associative and commutative the order does not matter. Exhausting all possible combinations with max, only the following frames are possible: PE , CB , CB , CE , RUN , CB , and RUN , CE .

Example 14 (Edit frames). We consider the pointcut expression: atLocation( 1 ) and write(x). These expressions have the frames PE , CB and CB , CE , respectively. This means that atLocation( 1 ) starts right after the previous transitions leading to 1 have finished executing their update function, while for write(x) it starts right after the transition executes (i.e., CB , at the start of its update function). Their combination must start when they both start, in this case CB . If we consider the start to be the earliest, then we can still pass PE but it is possible to execute another transition that does not match write(x). This is not consistent with the start of write(x). They both end after (1) atLocation( 1) is over and (2) write(x) is over, therefore they end when the transition ends (CE ).

Overview.. Recall from Definition 21 that both of the update functions F b and F a of an advice have read/write access to a component variables. It is also possible that F b and F a belong to different transitions. Therefore, it could be possible to update the variables in F b in a way that ensures F a is never executed. The first requirement of the weaving procedure is to ensure that F a will always execute once F b has executed.

Remark 3 (Deadlocks). It is ensured that function F a executes after F b if the user's advice does not result in a deadlock state. For example, the before computation may modify the state so as to have no outgoing enabled transition. Hence, the after computation is not executed. Since weaving transforms a BIP model, it is possible to use verification tools (such as DFinder [START_REF] Bensalem | D-finder 2: Towards efficient correctness of incremental design[END_REF]) on the transformed model to check for deadlock freedom.

In order to apply the requirement, the general weaving strategy uses one boolean variable per aspect b aop . The variable b aop is set to false right before reaching the joinpoint and set to true upon joinpoint entry, indicating a pointcut match. It is then up to the weaving procedure to unset if necessary. We use for brevity: F set = b aop := true and F clear = b aop := false . In addition to b aop we define the extra port ip. The ip port is associated with a singleton interaction with the highest priority in the system. It is used to create high priority transitions in the component creating deterministic behavior.

In the following, we begin by weaving the reset location pairs, since it is independent of execution frames. Later, we consider the weaving of the advice adv = F b , F a , {} on a set of transitions M for each of the four pairs of frames: PE , CB , CB , CE , RUN , CB , RUN , CE . We fix T and L to be the set of transitions and locations of the new atomic component respectively. A set of locations L R contains the locations (blocks) on which the pointcut ends, so that it is possible to weave the reset locations. An injective function m : B k .trans → 2 T relates B k .trans to the new transitions by transforming them, creating extra transitions or copying them.

Weaving reset location pairs.. We consider a set R of reset location pairs, and a set of locations L R . The reset location transitions are defined as follows:

wReset(R, L R ) = guard,dest ∈R ({ , ip, b aop ∧ guard, F clear , dest | ∈ L R }).
The transitions are guarded by b aop so as to execute only if the pointcut matched. They execute on ip so as to have priority over other transitions at the location. Once executed they invoke F clear to indicate that the pointcut has ended. Consequently it avoids a deadlock when the location resets to itself.

Example 15 (Weaving reset location). Figure 6 shows the weaving of reset locations, namely wReset({ 4 , g a , 1 , g b } , { 1 , 2 }). In total, four transitions are created as we have two locations and two reset pairs. Transitions are highlighted differently for each destination location.

We now elaborate on the weaving of each edit frame by detailing the transitions that are modified, the extra locations created and specifying which locations are selected to apply the reset location transformation on.

Weaving CB , CE .. The edit frame CB , CE applies at the level of transitions in M . Therefore, F b (resp. F a ) is simply added at the beginning (resp. end) of F , resulting in F = F b , F, F a . All transitions leading to the transitions in M , namely prev(M ) must invoke F clear 25 [g5] p2 f5

[g0] p1 f0

[g1] p1 f1

[g2] p1 f2

[g3] p2 f3

[g4] p2 f4 after finishing their computation. Care should be taken in the case of loops as they are both in the match and lead to the match. F set is executed to indicate that the joinpoint matched followed by F a . No additional locations are necessary, L = B k .locs. L R consists of the locations to which any transition in M leads, they are then dest(M ). We define m as follows:

t 5 t 0 t 1 t 2 t 3 t 4 p1 p2 B x 0 1 2 3 4 [g5] p2 f5 [g0] p1 f0 [g1] p1 f1 [g2] p1 f2 [g3] p2 f3 [g4] p2 f4 [baop ∧ ga] ip F clear [baop ∧ g b ] ip F clear [baop ∧ ga] ip F clear [baop ∧ g b ] ip F clear p1 p2 ip B x b aop
m(t = , p, g, F, ) =    { , p, g, F F clear , } if t ∈ prev(M ) \ M m { , p, g, F b F F set F a , } if t ∈ M, {t} otherwise.
The new set of transitions is then T = t∈B k .trans m(t). The whole procedure is defined as:

wframe cur (B k , M, F b , F a ) = T , L , L R , m .
Weaving PE , CB .. Both PE and CB apply at the level of transitions. PE indicates that F b must be woven on the transitions leading to those in M namely prev(M ), at the end of their update function. CB indicates that F a must be woven on the transitions in M , at the beginning of their update function. In this case, loops require more instrumentation. Let the set of loop transitions be T L = prev(M ) ∩ M , if we have such transitions T L = ∅, we create the set of extra locations L temp = ⊥ | ∈ origin(T L ) . For a given loop transition , p, g, F, , we set the update function to F a , F set , F and change the destination to ⊥ and add a transition that executes F b on port ip from ⊥ to . Thus if a reset location is to happen, it would happen on ⊥ , without executing function F b again.

L R = dest(M ) \ origin(T L ) ∪ L temp if T L = ∅ dest(M ) otherwise L = B k .locs ∪ L temp if T L = ∅ B k .locs otherwise m(t = , p, g, F, ) =        { , p, g, F F clear F b , } if t ∈ prev(M ) \ M , p, g, F a F set F, ⊥ if t ∈ M ∩ prev(M ) { , p, g, F a F set F, } if t ∈ M \ prev(M ) {t} otherwise T = {m(t) | t ∈ B k .trans} ∪ ⊥ , ip, true, F clear F b , | ⊥ ∈ L temp
The whole procedure is defined as:

wframe prev (B k , M, F b , F a ) = T , L , L R , m .
Weaving RUN , CB .. This frame requires block instrumentation to handle portEnabled. RUN indicates that additional computations needs to be handled. These computations refer to port enablement since only matching at least one port enablement can lead to RUN . In the first step, we define the selected ports. Selected ports are the ports matched as part of the pointcut expression lpc using sp(lpc) = match lpc with

|atLocation( ) → ∅ |readVarFunc(x ) → ∅ |readVarGuard(x ) → ∅ |write(x ) → ∅ |portEnabled(p) → {p} |portExecute(p) → ∅ |φ and φ → sp(φ) ∪ sp(φ )
First we begin by creating the guard expression for the enabled ports. A port p is enabled in a location if there exists at least one transition which guard evaluates to true. In the case of multiple ports, they must all be enabled.

mkGuard(SP, , M ) = p∈SP ( τ ∈M ∧τ.src= ∧τ.port=p (τ.guard ))
Second, since port enablement can be detected only when the guards are evaluated at the location, to execute function F b we need to pre-evaluate the guards before entering the location. To match a port enablement at a location , we create a temporary location ⊥ that pre-evaluates the guard. By applying this to the entire match M , we have L temp = ⊥ | ∈ origin(M ) . We then connect each ⊥ to with two transitions, the first executes F b and does F set , indicating the pointcut match, and the second does F clear . Both these transitions execute on ip so as to not be enabled or execute any existing port. The added transitions are:

T cr = ⊥ ( ⊥ , ip, g, F set F b , , ⊥ , ip, ¬g, F clear , with g = mkGuard(sp(lpc), , M ))
Third, since port enablement is determined dynamically, we simulate an if/else construct. Outgoing transitions from are duplicated. This results in two versions. The first checks for the joinpoint match (if b aop holds) and applies F a . The second checks for (b aop = false) and does not apply F a weaving in CB .

Lastly, all the incoming transitions from are redirected from to ⊥ so as to reach ⊥ to preevaluate the guard before . Thus, we get the resulting new set of locations L wand transitions

T . L = B k .locs ∪ L temp T = {m(t) | t ∈ B k .trans} ∪ T cr with t = , p, g, F, and
m(t) =    { , p, b aop ∧ g, F a F, , , p, ¬b aop ∧ g, F, } if t ∈ M , p, g, F, ⊥ if t ∈ prev(M ) \ M {t} otherwise 0 1 2 ⊥ 2 3 4 [g5] p2 f5
[g0] p1 f0

[g1] p1 f1

[g2] p1 f2

[g3] p2 f3

[g4] p2 f4

[gadd] ip FbFset [¬gadd] ip p1 p2 B x 0 1 ⊥ 2 2 3 4 [g5] p2 f5
[g0] p1 f0

[g1] p1 f1 In the case of loops, a reset location should happen on the temporary locations.

[baop ∧ g2] p1 Faf2 [¬baop ∧ g3] p2 f3
[¬baop ∧ g2] p1 f2 [baop ∧ g3] p2 Faf3 [baop ∧ g4] p2 Faf4 [¬baop ∧ g4] p2 f4 [gadd] ip FsetFb [¬gadd] ip Fclear p1 p2 ip B x baop
L R = dest(M ) \ origin(M ) ∪ L temp
The whole procedure is defined as: wframe runb (B k , M, F b , F a , lpc) = T , L , L r , m .

Example 16 (Dynamic weave). Figure 7 depicts the weaving of the advice F b , F a , ∅ with the pointcut lpc = atLocation( 2 ) and portEnabled(p 1 ) and portEnabled(p 2 ). The selected ports are sp(lpc) = {p 1 , p 2 }, the origin is determined, origin({t 2 , t 3 , t 4 }) = { 2 }. The condition for the enabled ports is: g add = mkGuard({p 1 , p 2 } , 2 , {t 2 , t 3 , t 4 }) = g 2 ∧ (g 3 ∨ g 4 ). Both ports {p 1 , p 2 } are enabled when p 1 is enabled (g 2 is true) and p 2 is enabled (g 3 ∨ g 4 is true). We create a set of temporary locations: L temp = ⊥ 2 . Two transitions are created per location. The first executes iff the ports are both enabled (pointcut matched), its update function is F b and F set . The second executes iff one of the ports is not enabled (pointcut not matched), its update function does F clear . Transitions with 2 as destination are redirected to ⊥ 2 . Then, we copy over the originally outgoing transitions from 2 , creating two versions of them: one has F a and is guarded by b aop and another executes normally and is guarded by ¬b aop .

Weaving RUN , CE .. The frame is woven similarly to RUN , CB . The RUN edit point indicates that portEnabled must hold, so the transformations described in the previous part are similar. However, we modify the order of execution of F b and F a . Since F b executes on CB , we do not execute it on the added transitions that detect port enabled.

T cr = ⊥ ( ⊥ , ip, g, F set , , ⊥ , ip, ¬g, F clear , with g = mkGuard(sp(lpc), , M )).
Instead, F b needs to be added to the transition which matches the port enablement. Therefore, F b and F a are added to the duplicated transitions that match the guard g.

L = B k .locs ∪ L temp T = {m(t) | t ∈ B k .trans} ∪ T cr with t = , p, g, F, and
m(t) =    { , p, b aop ∧ g, F b F F a , , , p, ¬b aop ∧ g, F, } if t ∈ M, , p, g, F, ⊥ if t ∈ prev(M ) \ M, {t} otherwise.
When considering reset location, loops and temporary locations must be adjusted similarily to weaving RUN , CB :

L R = dest(M ) \ origin(M ) ∪ L temp
The whole procedure is defined as:

wframe runa (B k , M, F b , F a , lpc) = T , L , L r , m .
Weaving a local aspect.. The local weave operation weaves an advice on set of transitions M with the set of intertype variables V and a local pointcut expression lpc.

Definition 24 (Local Weave). The local weave is defined as:

C , m = weave (C, B k , V, lpc, M, ladv(B k , V ) = F b , F a , R )
where

C = π(γ ((B \ B k ) ∪ B k ))
is the resulting composite component; with:

• B k = P ∪ {ip} , L , X ∪ V ∪ {b aop } , T ∪ T R is the resulting atomic component;
• b aop is the aspect boolean variable described earlier;

• T , L , L R , m =        wframe cur (B k , M, F b , F a ) if edit(lpc) = CB , CE wframe prev (B k , M, F b , F a ) if edit(lpc) = PE , CB wframe runb (B k , M, F b , F a , lpc) if edit(lpc) = RUN , CB wframe runa (B k , M, F b , F a , lpc) if edit(lpc) = RUN , CE • T R = wReset(R, L R ) is obtained from weaving reset locations; • γ = γ ∪ {a ip } where a ip = ip, true,
is the high priority interaction for the aop port;

• π = π ∪ { a, a ip | a ∈ π} is the new set of priorities.
Weaving a local aspect on a composite component C = π(γ(B)) is defined as:

C = C B k ∈ B, lpc, V, ladv(B k , V )
where: C is the result from the local weave:

C , m = weave (C, B k , V, lpc, select (B k , lpc), ladv(B k , V )).
The new atomic component B k has one extra port (ip), and has B k .vars ∪ V ∪ {b aop } as the set of variables. The edit frame is determined using operator edit (Definition 23) and transitions and locations are instrumented accordingly. The obtained composite component C has one extra singleton interaction a ip associated with port ip. Additionally, interaction a ip is given the highest priority w.r.t. predefined interactions. 29

Correctness of local weave.. Informally, to verify the correct addition of the advice w.r.t joinpoint matching, we need to first verify that the before and after update functions were placed correctly when a joinpoint is matched during runtime. This is similar to the correctness of global weaving expressed in Proposition 2. However, we note that the before update function (F b ) must, in some cases, execute in the local event preceding the match. Secondly, in the presence of reset location, the local event succeeding the matched event should indicate that the local component is in the appropriate location. As such, the order of the events is also checked in the case of local weaving.

We first need to make the distinction between the frames that weave F b on the previous transitions with those that do not.

We define predicate early(lpc) = false if edit(lpc) ∈ { CB , CE , RUN , CE } , true otherwise. We consider E k (resp. E k ) to be reachable events in B k (resp. B k ). We define rem k :

E k × F × F → E k ∪ { },
the function that removes the local advice from a local event.

rem k ( l, v , τ, q , F b , F a ) = l, v , τ , q if l ∈ B k .locs, otherwise.
The constructed event is the following:

• v excludes the valuations of the inter-type V from v while the location is maintained.

• If the event has a location not found in B k .locs, then a similar event cannot be constructed. The resulting event is .

• τ = l, τ.port, g, F, l is the similar transition where g does not contain b aop , F does not contain F set , F clear , F b , F a and l is any location (since q is never matched against a joinpoint so it is not relevant).

By removing the advice, we ensure that lpc must not match read/writes introduced by F b and F a . We use before(e i , F, d) and after(e i , F, d) where e i is a local event, F is the before or after update function, and d is the value of the predicate early, to verify the correct application of the before and after update functions respectively.

before(e

i , F, d) iff (b ∧ i = 0 ∧ ∃F : e i-1 .τ.func = F , F ) ∨ (¬b ∧ ∃F : e i .τ.func = F, F ) after(e i , F, d) iff (b ∧ ∃F : e.τ.func = F, F ) ∨ (¬b ∧ ∃F : e.τ.func = F , F )
In the case where the predicate early(lpc) holds, the predicate before(e i , F, d) checks if the function of the preceding event's update function (e i-1 .τ.func) ends with F , with the exception of the first event (i = 0), while the predicate after checks that the current event's function (e i .τ.func) starts with F . In the case where the predicate early(lpc) does not hold, the predicate before (resp. after) ensures that the current event's update function (e i .τ.func) starts (resp. ends) with F .

For the case of a reset location pair r = guard , loc we check if its guard holds trueon the next event. If it does, we verify that the location e i+1 .l is the destination location in a reset location pair.

reset(e i , r) iff (guard(e i+1 .v ) =⇒ e i+1 .l = loc)

We can now express the correct application as follows:

(e i = ∧ e i lpc) iff before(e i , F b , d) ∧ after(e i , F a , d) (1)
(e i = ∧ e i lpc) =⇒ (R = ∅ =⇒ ∃r ∈ R : reset(e i , r)) (2)
We begin by constructing an event e i = rem k (e i , F b , F a ) from e i by removing the local advice. The proposition states that e i is a joinpoint (e i lpc) in the original system iff the update function associated with e i verifies the rules for before (before(e i , F b , d)) and after (after(e i , F a , d)). In the presence of reset location pairs (2), if the event e i is a joinpoint in the original system, the next event includes at least one reset location pair (R = ∅ =⇒ ∃r ∈ R : reset(e i , r)).

Weaving Strategies

An aspect is the single association of a pointcut expression to a joinpoint. However, when weaving more than one aspect, specific problems and extra considerations arise. This section identifies possible issues when weaving multiple aspects and presents two basic procedures to coordinate the weaving.

Furthermore, this section can be seen as a preliminary method to provide a grouping of aspects and basic strategies for weaving them. It can be seen as the interface between the user and the transformations described earlier in the paper for the two views. As such, while we present a basic overview of the strategies to combine and weave multiple aspects, we note that it is possible to use the transformations to build more complex ones that best suit the users' needs.

Interference

Recall that multiple concerns may happen at one joinpoint. This can be seen as the tangling phenomenon. When a new concern is added to the joinpoint, it is possible to have existing concerns at the same joinpoint. This situation is referred to as interference. Since not all concerns are independent, interference is an important issue to study.

Example 17 (Interference). Consider gpc = {p 1 } , ∅, ∅ , V = {x}, the two global aspects GA 1 = C, V, gpc, F b = x := 3 , F a , and GA 2 = C, V, gpc, F b = x := 2 , F a . Both of these aspects' advices operate on the same inter-type variable x and on the same matched joinpoints. There are four possibilities for weaving the advices, depending on the order of F b , F b , F a and F a . In the case of F b and F b if we have F b , F b (resp. F b , F b ) then x will be 2 (resp. 3) at runtime.

Defining weaving strategies helps to deal with interference in a more predictable way. To do so, we examine in the following: (1) a modular unit that groups aspects, and (2) the operations that weave multiple aspects.

Containers

Aspect containers encapsulate a group of aspects. Local containers (resp. global containers) apply to local (resp. global) aspects. Aspect containers seek to group interfering aspects and define extra restrictions so as to manage their weaving. By doing so, we expose multiple aspects to the user as a coherent unit.

Definition 25 (Global and local containers).

A global container is a tuple GA 1 , . . . , GA n , V such that any GA j ∈ {GA 1 , . . . , GA n } has the inter-type V . A local container is a tuple LA 1 , . . . , LA m , B, V such that any LA i ∈ {LA 1 , . . . , LA m } is applied to an atomic component B and has the inter-type V .

Containers define an order on the aspects they encapsulate. They permit the definition of a weaving order for aspects. Moreover, containers ensure that aspects share the same inter-type variables. Sharing allows the inter-type to be encapsulated in the container. In the case of local containers, local aspects are required to operate on the same atomic component encouraging encapsulation. The local aspects operating on different atomic components do not interfere and cannot share inter-type variables.

Weaving Procedures

The weaveSerial procedure.. Given a global or local container, one example of weaving procedure weaves aspects in the order they are contained. The aspects are presented in a sequence asp 1 , . . . , asp n where asp 1 , . . . , asp n are all either global or local aspects.

Definition 26 (weaveSerial). Depending on the aspect type we have two operations:

• The procedure weaveSerial applied to a sequence of local aspects asp 1 , . . . , asp n is:

C = weaveSerial (C, asp 1 , . . . , asp n ) = ((((C asp 1 ) asp 2 ) ..) asp n )
• The procedure weaveSerial g applied to a sequence of global aspects asp 1 , . . . , asp m is:

C = weaveSerial g (C, asp 1 , . . . , asp m ) = ((((C g asp 1 ) g asp 2 ) g ..) g asp m )
The weaveSerial procedure allows the pointcut of any aspect asp i (i ∈ {2, . . . , n}) to match changes introduced by all aspects asp j prior to it (for j < i).

While Definition 26 presents a simple weaving strategy, we can consider alternative strategies. Firstly, we can consider that the matching of the pointcut and the weaving are separate. This is the case for weaveAll presented in the next paragraph. Secondly, we note that it is possible to modify the order of the aspects in the sequence. For example, it is possible to order aspects by (1) the type of the pointcut's edit frame or (2) by whether or not their advice performs only read or also modifies the variables.

The weaveAll procedure.. The weaving procedure for local aspects introduces new locations and transitions in the cases of reset locations and port enabled. The second compositional approach weaveAll allows the pointcut of a local aspect asp i in the sequence to not match extra transitions added by asp j (for j : j < i). While weaveSerial can be seen as iteratively doing match and weave for each aspect, weaveAll makes it is possible to match the joinpoints of the entire sequence of aspects before weaving them. The procedure weaveAll matches all the pointcuts of the sequence, then weaves the aspects according to their order based on their original match projected onto the new component. For a local aspect LA = B, pc, V, F b , F a , R we denote B, pc, V, F b , F a , R by LA.B , LA.pc, LA.V and LA.adv , respectively.

If we consider two local aspects asp 1 , asp 2 and their local pointcut matches M 1 and M 2 respectively. Weaving asp 1 on its match M 1 , using weave (C 0 , asp 1 .B, asp 1 .V, asp 1 .pc, M 1 , asp 1 .adv), results in C 1 , m 1 . The weaving of asp 2 needs to apply on C 1 and not on C 0 on which asp 1 .pc was matched. Therefore its original match M 2 needs to apply to transitions in C 1 as the local weave could change the transitions. To do so we use the transformation function m 1 (see Definition 24) to get the transitions in C 1 from C 0 . Therefore the new set of matches in C 1 given M 2 is determined using newM(M 2 , m 1 ). newM(M, m) = {m(t) | t ∈ M } Since m applies only to one weave, we generalize it to the k th weave by successive application over the k -1 weaves using m 1 . . . , m k-1 .

follow(M, m 1 , . . . , m k-1 ) = newM(newM(newM(M, m 1 ), . . .), m k-1 ) k -1 > 1 M otherwise
Definition 27 (weaveAll). The weaveAll for a sequence of n local aspects on a composite component C 0 is defined recursively as C n , m n = weaveAll(C 0 , asp 1 , . . . , asp n ) such that ∀i ∈ {1, . . . , n}:

C i , m i = weave (C i-1 , f ollow(M i , m 1 , . . . , m i-1 ), asp i .V , asp i .adv ) M i = select (C 0 , asp i .pc)
Example 18. Figure 8 shows the different results obtained by weaving two local aspects a and a with the two proposed procedures. The pointcuts are a.pc = (atLocation( 0 ) and portExecute(p 2 )) and a .pc = atLocation( 1 ). The corresponding advices are a.adv = F b , F a , { 0 , true } and a .adv = F b , F a , {} .

• Figure 8a and Fig. 8b show the weaving of each aspect individually. Let M (resp. M ) be the match of a.pc (resp. a .pc) and t 5 the transition guarded by g 5 , t 5 is both in M and prev(M ). In this case, the advices from a and a overlap when woven on t 5 .

• Figure 8c and Fig. 8d illustrate the weaveSerial operation.

1. Figure 8c presents the serial weave of a followed by a . The weave of a results in C 1 , m 1 . C 1 is shown in Fig. 8a. Upon weaving a its pointcut will match the reset location as it is outbound from 1 and will therefore prepend F a to it. The pointcut will also match m 1 (t 5 ) as it is inbound, therefore it appends F b , F clear to its existing function ( F b , f 5 , F set , F a ) on which a was already woven.

2. Figure 8d presents the serial weave on a followed by a. The weave of a results in C 1 , g 1 . The component is shown in Fig. 8b. Upon weaving a the pointcut will match m 1 (t 5 ). Its function f 5 , F b , F clear is then appended with F a , F set . Additionally, the reset location is then added guarded by b ∧ true.

• Figure 8f illustrates the weaveAll operation and how it differs from weaveSerial. The pointcut of a will always match against the original component, matching always the transition guarded by t 5 . The weaveAll procedure projects the match. The new match result will be t 5 if a is woven first or m 1 (t 5 ) if a is woven first. The joinpoint will therefore not contain the reset location in both cases. The order of the aspects still defines the order of the advices woven on overlapping transitions. Fig. 8e displays the different advice order. Reset location.. In both cases, whenever multiple reset locations are woven on the same location, they are all woven with an extra port appended to the component (the ip port). Since at every weave a singleton interaction has the highest priority, the last local aspect in the sequence has the highest priority on their port. Thus, if multiple reset locations are found on one location (and all their guards evaluate to true), the reset location that was woven last will always execute. In the case of weaveSerial, it is possible to match the transitions that originate in the intermediary location, and thus can include different reset locations than expected. Since aspects are assumed to be woven on a new system at every iteration, it is possible to have reset locations on intermediary states created by portEnabled. This could cause undesirable side effects, such as weaving on different locations or transitions (as shown in the following example). By defining more elaborate weaving strategies, one can better manage the expectations of the user and define properties that are preserved or affected by the interference.

0 1 2 [g5] p2 Fbf5FsetFa [g0] p1 f0 [g1] p1 f1 [b] ip Fclear p1 p2 ip x b (a) Weaving a 0 1 2 [g5] p2 f5F clear F b [g0] p1 f0 [g1] p1 F a F set f1 p1 p2 ip x b (b) Weaving a' 0 1 2 [g5] p2 Fbf5FsetFaF clear F b [g0] p1 f0 [g1] p1 F a F set f1 [b] ip F a F set Fclear p1 p2 ip x b b (c) weaveSerial a, a 0 1 2 [g5] p2 Fbf5F clear F b FsetFa [g0] p1 f0 [g1] p1 F a F set f1 [b] ip Fclear p1 p2 ip x b b (d) weaveSerial a , a 0 1 2 [g5] p2 Fbf5FsetFaF clear F b [g0] p1 f0 [g1] p1 F a F set f1 [b] ip Fclear p1 p2 ip x b b (e) weaveAll a, a 0 1 2 [g5] p2 Fbf5F clear F b FsetFa [g0] p1 f0 [g1] p1 F a F set f1 [b] ip Fclear p1 p2 ip x b b (f) weaveAll a , a
Example 19 (Reset location interference). Figure 9 shows interference when weaving two local aspects a and a on a base component B (shown in Fig. 9a). The pointcuts expressions for a and a are respectively : portEnabled(p 1 ) and readVarGuard(x). Both a and a use the same reset location set: { 0 , x < 5 }. In this case, we match the transition and create the addi-

0 1 [x ≥ 0] p1 f1 B (a) Base ⊥ 0 0 1 [x ≥ 0] p1 f1 [(x ≥ 0)] ip Fset [¬(x ≥ 0)] ip Fclear [baop ∧ x < 5] ip Fclear B (b) Weaving a ⊥ 0 0 1 [x ≥ 0] p1 f1 [(x ≥ 0)] ip Fset [¬(x ≥ 0)] ip Fclear [baop ∧ x < 5] [g2] [g3] []

B

(c) Weaving a' tional location ⊥ 0 as shown in Fig. 9b. However, when matching readVarGuard(x) on B , all transitions (including created ones) match since they contain x in their guards. In this case the destination locations are ⊥ 0 , 0 and 1 . Thus, three transitions to 0 are then created (one from each destination location) when weaving a as shown in Fig. 9c. In this case we note that the transitions are not created on ⊥ 0 and execute before the reset location of a. A side effect of the new reset location transitions makes it possible to completely skip evaluating the portEnabled pointcut while moving from ⊥ 0 to 0 .

Remark 4 (Strategies and properties). While we explored specific procedures to weave aspects, and possible issues that are generated from weaving multiple aspects, we stress that for the current work we consider each weave to be on a fresh component. Thus, in our view, the designer, when weaving multiple aspects, is actually looking at the changes in the system from each single weave and determining what should be woven next.

AOP-BIP: Aspect-Oriented Programming for BIP Systems

We present AOP-BIP, a prototype tool that implements our approach. To test our approach we consider first a network protocol then show the applicability of our approach to monitor CBSs. We begin by describing the network protocol using BIP. Then, we identify cross-cutting concerns and describe them using the AOP-BIP language. Finally, we instrument the network model to include these concerns using the AOP-BIP tool. We illustrate the weaving of each concern by looking at scattering and tangling. Scattering is measured by counting the elements (affected transitions or interactions in the model) which contain the concern, while tangling is measured by counting the number of elements on which multiple concerns overlap. The scattering and tangling of a concern serve as an indicator of the complexity to implement a concern manually without using AOP-BIP tool.

Tool Overview

AOP-BIP is a proof-of-concept, aspect-oriented extension to BIP written in Java (∼ 4300 LOC).

Using the AOP-BIP tool.. The command-line front end of AOP-BIP takes as input:

• A .bip file that represents a BIP system written in the BIP language [START_REF] Verimag | BIP Tools[END_REF];

• The name of the weaving procedure to apply when weaving the aspects on the BIP model;

• A list of .abip files that describe the aspects.

AOP-BIP produces the BIP model and the aspect containers by parsing the .bip file and .abip files, respectively. It selects a weaving procedure to compose the aspects per container as described in Section 7. AOP-BIP then weaves the containers onto the BIP model resulting in an output BIP model.

Overview of the AOP-BIP language.. The BIP language is described in full in [START_REF] Verimag | BIP Tools[END_REF]. We use only a subset of the language to illustrate the concepts of this paper. The BIP language is typed. Components, ports and data are associated with types. In addition to a description of the BIP system, .bip files also contain a module declaration to encapsulate the system and a header section. The header contains arbitrary C code that is used during code generation.

The AOP-BIP language follows the same ideas presented in this paper with a few extensions. 2 At the file level an AOP-BIP file contains a header followed by multiple containers. The header provides additional C code to merge with the .bip header. This is useful to define extra functions or include extra libraries. Aspects are grouped into containers. A container is defined by declaring the Aspect keyword followed by its identifier3 . If the container defines local aspects, then it must specify the atomic component it targets right after its identifier. The intertype variables are not included in the individual aspects, but at the container level. We select an atomic component or an interaction by its identifier in the system. Therefore, local aspects apply to a specific instance of the atomic type and global aspects apply to a specific instance of the connector type. The global pointcut syntax includes a port specification: portspec. The port specification is used to alias a port identifier. For example, using the specification p : c1.stop allows the port stop in component c1 to be referenced as p in the rest of the pointcut or the advice, if c1.stop has a variable x, it can be referenced as p.x. This is provided merely as syntactic sugar to simplify referring to the port variables in the read and modified variables in the pointcut and the advice's update functions.

The Network Example

A network protocol is used to illustrate the handling of crosscutting concerns in BIP and is shown in Fig. 10. The network protocol is an augmented version of the one presented in [START_REF] Bonakdarpour | A theory of fault recovery for component-based models[END_REF]. The Network composite component consists of a Server, a Client and a Channel. The double circles denote the start locations for each component. The Server waits for the clear-to-send signal on its cts port. This indicates that a channel is available. It then generates a packet and sends it to the channel. The channel forwards the packet to the client which acknowledges it. The channel will then send the acknowledgement back to the server. Crosscutting concerns.. The network protocol is augmented by refining its specification. The correctness of our transformation ensures that the crosscutting concerns are rigorously handled. First, logging is introduced by capturing port executions locally in all components. Second, security is added in the form of authentication. A signature (hash) is added to the packet and checked. To accomplish the above we introduce two local aspects. The various aspects along with the output are displayed in Fig. 11. The first intercepts the Server's cts port execution and adds the signature once the server is ready to send, by modifying the packet stored in the local variable p. The second intercepts the Channel's add1 port execution; this port executes when a packet from the Server is sent. The advice verifies the signature (using check(p)) and stores the result (logical 0 or 1) in an inter-type variable clear. The advice also adds a reset location to IDL if the verification failed (clear == 0), preventing the Channel from forwarding the packet to the Client. The Carol aspect is added to modify the packet in transit to display a failed authentication. The global pointcut expression matches: (1) ports server.send and channel.add1, and (2) variable server.send.r. The advice in the Carol aspect changes the value of channel.add1.r after the execution of any interaction that matches the pointcut. Normally, the system executes the packet transfer by reading a.r and modifying b.r. The advice function instead will override b.r by generating a fake packet from a.r using pfake(a.r). The output displays a successful and an unsuccessful attempt. The packet is represented by a number and the signature is the last digit in the number. We notice that the first aspect added |6 to the packet 886 and the second aspect removed it when the channel forwarded it (Channel1.rem1). Carol replaces the first packet 886 with 386, which both have the same signature [START_REF] Bauer | Runtime verification for LTL and TLTL[END_REF]. The verification succeeds in this case unlike in the second try, when 763 is replaced by 736 since the signature of 736 is 6 but not 3. Third, congestion avoidance is added by computing the round-trip time of the message and then waiting before sending further messages. Fourth, basic fault tolerance is introduced in the form of a failsafe mechanism. The system deadlocks and then terminates safely, after the server fails to receive a certain number of acknowledgments.

Coverage of concerns.. The coverage of the concerns is shown in Table 2. Column Transitions reports the number transitions that have been modified including the number of added transitions for reset locations. Column Interactions reports the number of modified interactions. Column OT (resp. OI) reports the number of transitions (resp. interactions) that overlap with other concerns. Interfering concerns are reported in column OC. Concerns are indicated by label [START_REF] Aksit | An object-oriented language-database integration model: The composition-filters approach[END_REF][START_REF] Altisen | Aspect-oriented programming for reactive systems: Larissa, a proposal in the synchronous framework[END_REF](3)[START_REF] Bartocci | Introduction to runtime verification[END_REF]. We illustrate concerns that target multiple areas in the system. Without using AOP-BIP, implementing these concerns would require one to edit a significant part of the system. For instance, in the case of logging, the code must be inserted in 10 transitions, of which half overlap with other concerns.

Applicability to Runtime Verification of CBSs

Overview. Runtime verification (RV) is a lightweight verification technique used to verify whether a run of a specific system verifies a specific property [START_REF] Falcone | A tutorial on runtime verification[END_REF][START_REF] Bartocci | Introduction to runtime verification[END_REF]3]. It consists in extracting a sequence of events, which is then fed to a monitor that verifies it against a specification. RV frameworks for CBSs, and particularly for BIP systems (RV-BIP [START_REF] Falcone | Runtime verification of component-based systems in the BIP framework with formally-proved sound and complete instrumentation[END_REF] and RVMT-BIP [START_REF] Nazarpour | Concurrency-preserving and sound monitoring of multi-threaded component-based systems: theory, algorithms, implementation, and evaluation[END_REF]) have been already developed. They define specific transformations to instrument components and insert monitors as components in the new system (RV-BIP for sequential systems and RVMT-BIP for multi-threaded systems). However, since runtime verification is a crosscutting concern, it is possible to instrument a system with aspects (both global and local) to generate necessary events for monitoring. At the global level, it is possible to monitor interactions by intercepting their ports and variable accesses. Thus, by describing global pointcuts, we can generate events that are global, and synthesize global aspects that implement monitors. Since we allow for inter-type declarations at the global level, a monitor state can be stored in the inter-type component. The component can then be used to describe a specification for a monitor. At the local level, it is possible to monitor the component state by using local pointcuts. Thus we can generate events that are local to the component. Using local aspects, we can then describe local monitors that are embedded in the component to check for local events. Certain properties however require information from multiple local monitors, thus it is impossible to handle the synchronization with our current approach. Directly writing monitors as aspects is not handled for these types of properties. However, it is possible for each local monitor to print out an event, and a separate monitoring mechanism to verify the entirety offline. While we do not tackle the automatic synthesis of monitors from a specification, we show next how AOP-BIP can be used to write manual monitors for specific properties.

Dala robot. A robotic application is used as an example in [START_REF] Falcone | Runtime verification of component-based systems in the BIP framework with formally-proved sound and complete instrumentation[END_REF]. The Dala robot [START_REF] Fleury | G en om: a tool for the specification and the implementation of operating modules in a distributed robot architecture[END_REF] is a large and realistic interactive system which consists of a set of modules. Each module is a set of services that corresponds to different tasks and a set of posters that are used to exchange data with other modules. A simplified simulation of the modules consists of various services classified as readers and writers accessing data of a poster component and a global clock component clock.

Reader services read the data in the poster, and writer services modify it. A writer simulates a large data transfer consisting of two phases. In the first phase, the writer writes a task id to the poster using an interaction that exchanges the task id between the two ports: writer.writev, and poster.writev. We assume that the task ids represent an abstract workload assigned to the various services and components of the robot. Upon completion, the interaction consisting of the ports writer.finishWrite and poster.finishWrite is executed. We use the example to monitor the following properties: mutual exclusion between writers, data freshness and ordering of tasks. The monitors are presented in Listing 3.

Monitoring mutual exclusion. The first property focuses on writers. The writing process consists of two steps: write and finishWrite. The writev port is triggered when a writer starts writing to the poster service, and upon completion finishWrite is executed. The property checks that no two writers are writing at the same time. To monitor the property, we create a local aspect on the poster component, and use an extra inter-type variable c initialized to zero. Upon execution of the port writev, we check if c is non-zero and increment it by one, and upon execution of the port finishWrite we decrement c by one. Thus, if two executions of the port writev happen, the monitor can verify the property (c > 0).

Monitoring freshness. The second property focuses on readers, when a reader reads data posted by a writer, the freshness property checks for constraints on timestamps. The goal is to make sure that the data being read is up-to-date, i.e. the data has been read at most after a fixed amount of ticks. To do so, the property compares the timestamp stored in the poster against the current timestamp stored in the clock component, whenever a reader reads data. Thus, our monitor considers the interaction consisting of the ports reader.read, poster.read and clock.getTime.

The monitor intercepts the port variables to get the timestamp, then computes the difference and verifies whether it is below a threshold of 2 ticks.

Monitoring ordering. The third property concerns the interaction between the writers and the poster; when a task id is set, the ordering property expresses constraints on the order of tasks. In this example, we check if a task with a larger id executes before one with a smaller id. To do so, we use an inter-type variable lastTask and initialize it to zero, indicating that the next expected task is 1. We intercept all the interactions that involve the port poster.writev and check for those that write to the port variable (which contains the task id). In this case, the global advice is executed after the call, so as to catch the value written to the port's variable. Upon writing to the variable we check if the new task is in the correct order by comparing it to lastTask + 1 and then store the new task id as the lastTask.

Related Work

Modularizing AOP.. Multiple approaches have sought to (i) improve the applicability of AOP, and (ii) enhance its modularity. These approaches include, but are not limited to Ptolemy [START_REF] Rajan | Ptolemy: A language with quantified, typed events[END_REF], XPIs [START_REF] Sullivan | Modular aspectoriented design with xpis[END_REF], AspectJML [START_REF] Rebêlo | Aspectjml: Modular specification and runtime checking for crosscutting contracts[END_REF], and using substitution [START_REF] Molderez | Modular Reasoning in Aspect-Oriented Languages from a Substitution Perspective[END_REF]. They mainly focus on defining contracts and improving matching and advice applications in a modular way, and provide a better decoupling mechanism for the aspects of the systems. These approaches provide us with a perspective on how to better integrate, in a component-based manner, aspects in CBSs. However, they were mainly conceived to improve on the initial AOP methods that target non-CBS systems (i.e., AspectJ [START_REF]The AspectJ (TM) Programming Guide[END_REF]). They perceive the system as arbitrary function calls or message passing between objects that is not constrained. As such, they do not inherently target component-based semantics, such as synchronization or data transfers between various modules.

AOP for CBSs.. Pessemier et al. [START_REF] Pessemier | A component-based and aspect-oriented model for software evolution[END_REF] present a framework to deal with crosscutting concerns in CBSs. It is a symmetric approach, i.e. it uses the same language of the system to describe AOP concepts. It presents aspects as components containing the advice and additional interfaces, and are therefore integrated homogeneously within the system. Interaction with the advice is done through these added interfaces. The implementation of a concern is found in what is called an aspect component. Aspect components are regular components augmented with extra interfaces.

and after execute upon synchronization of all involved components. Similarly, other works such as [START_REF] Duclos | Describing and using non functional aspects in component based applications[END_REF] and [START_REF] Lieberherr | Aspectual collaborations: Combining modules and aspects[END_REF] integrate AOP into CBSs as well. These approaches are, however, asymmetric (i.e., they use an external language to represent AOP concepts) and subsumed by [START_REF] Pessemier | A component-based and aspect-oriented model for software evolution[END_REF]. Duclos's approach [START_REF] Duclos | Describing and using non functional aspects in component based applications[END_REF] defines two languages to integrate aspects. Lieberherr's approach [START_REF] Lieberherr | Aspectual collaborations: Combining modules and aspects[END_REF] defines aspects as part of the modules they apply to, and compares the expressiveness of the approach with both AspectJ and HyperJ [START_REF] Ossher | Hyper/J: Multi-dimensional separation of concerns for Java[END_REF].

SAFRAN [START_REF] David | An aspect-oriented approach for developing self-adaptive fractal components[END_REF] differs from the above approaches by using AOP in the Fractal component model to define adaptation policies.

Formalization of aspects.. The aforementioned approaches for CBSs do not rely on formal models. Work to formalize aspects in programs has been undertaken by [START_REF] Katz | Aspect categories and classes of temporal properties[END_REF]. The approach specifies different categories of aspects and how they affect various classes of properties (safety, liveness). Aspects are then assigned to a category by syntactic analysis. The work has been extended by Djoko et al. [START_REF] Djoko | Aspects preserving properties[END_REF] by expanding the categories and defining languages of aspects. The languages of aspects ensure by construction that aspects written with them fit a specific category. Additional tools for verification and analysis of aspects and their interference have been developed and are presented in [START_REF] Katz | The common aspect proof environment[END_REF]. The approach focuses on object-oriented systems, and not component-based systems, but it also provides theoretical results on property preservation which our approach does not study. By formalizing aspects in the context of CBS semantics, our approach paves the way to extend these works to CBSs.

Larissa [START_REF] Altisen | Aspect-oriented programming for reactive systems: Larissa, a proposal in the synchronous framework[END_REF] is a language for handling crosscutting concerns in reactive systems modeled as the composition of Mealy automata. The matching is done by assigning monitor programs that look for a specific execution trace. Joinpoints are then associated with the input history. Advices consist of two types: toInit and recovery. The toInit advice places the program back in its original state. The recovery advice consists of restoring the program to the last recovery state it was in. Since it is impossible to play the input backwards for recovery, a set of global recovery points is determined. A recovery state is determined by a monitor: the recovery program. The recovery states are associated with specific execution traces and are matched similarity to joinpoints. Compared to our approach, Larissa supports joinpoints based on the input history. It can also be seen as symmetric since aspects are introduced in the synchronous language used. However, the underlying model is conceived for reactive systems, and not CBSs, it does not have a clear distinction between communication and components, and thus does not distinguish between aspects related to components and communications. The communication model is based on simple input/output matching. Moreover, advices are not expressive and only consider reset/restore the state of the system. Formalizing aspects in the BRIC component model has been undertaken by [START_REF] Dihego | Aspect-oriented development of trustworthy component-based systems[END_REF]. BRIC formalizes the behavior of components and their interactions using the Communicating Sequential Processes (CSP) language. Unlike our approach, BRIC is symmetric: aspects, pointcuts, and advices are described in CSP, and woven using CSP operators. Additionally, BRIC targets interactions and not the components themselves. It regards components as black boxes. Similarly to BIP, CSP benefits from compositional verification of the properties and has a well-defined semantics. CSP uses denotational semantics as opposed to BIP which uses operational semantics. Verification on the resulting woven system is possible in both approaches. However, BIP has a strong expressive synchronization primitive [START_REF] Bliudze | A notion of glue expressiveness for component-based systems[END_REF] which is more expressive than CSP [START_REF] Hoare | Communicating Sequential Processes[END_REF]. This allows more concerns to be formalized.

Conclusions

Summary

This paper deals with crosscutting concerns in CBS using the AOP paradigm. It targets the two stages in the construction of CBSs by defining local and global aspects to refine components and their compositions, respectively. Local joinpoints capture concerns found in local components. Local pointcuts select joinpoints based on location, guards, variables in update functions and ports. They are associated with advices to add extra functionalities (e.g., computation or location change). Global joinpoints capture the interactions between components through their interfaces without having information about the internal representation of components. Global pointcuts select global joinpoints based on interactions, by considering ports and their respective data transfer operations. They are associated with global advices, to add extra functionality to the interaction model (e.g., data transfer, storing global information, etc.). Furthermore, to remedy interference and to increase expressiveness, we present a way to compose multiple aspects. Global and local joinpoints are mapped to BIP semantics and pointcut matching and advice weaving are implemented using model-to-model transformation on BIP models. We implement the proposed method in the AOP-BIP tool-chain. AOP-BIP consists of a language to describe both local and global aspects and provides an implementation of matching, weaving and composition. We study the automatic integration of various crosscutting concerns (logging, security, performance, fault handling) on a given input BIP system. Furthermore, we focus on a particular crosscutting concern, namely runtime verification and use AOP-BIP to monitor three properties on a robotic application designed as a CBS.

Future Work

Future work comprises four directions. The first consists in capturing more joinpoints and extending the possible behavior of advices. This would facilitate, in particular, the support for runtime verification [START_REF] Falcone | A tutorial on runtime verification[END_REF][START_REF] Bartocci | Introduction to runtime verification[END_REF] and runtime enforcement [START_REF] Falcone | You should better enforce than verify[END_REF][START_REF] Falcone | What can you verify and enforce at runtime?[END_REF], possibly in a timed setting [START_REF] Colombo | Safe runtime verification of real-time properties[END_REF][START_REF] Bauer | Runtime verification for LTL and TLTL[END_REF][START_REF] Pinisetty | Runtime enforcement of timed properties revisited[END_REF][START_REF] Falcone | Runtime enforcement of regular timed properties by suppressing and delaying events[END_REF] where the elapsing of physical time influences the behavior of monitors. Possible new joinpoints include variables in interaction guard, specific values of variables. Advices can be extended to modify guards on matching transitions and interactions. The second consists in applying CBS methods to define advices and aspect composition. This would help integrating AOP in BIP symmetrically, where aspects are implemented as components and interactions within the existing system. Moreover, this would allow to enable or disable aspects in the system, and specify more complex advices (i.e., advices as components instead of update functions and extra transitions). The third consists in elaborating new ways to compose aspects by finding new criteria to order them. Aspects can be re-ordered in a container based on their pointcut expressions, by grouping those that affect the same transitions or interactions, and whether or not they modify the existing variables (read/write aspects). Additionally, the language could be extended to allow the explicit definition of precedence rules. The fourth consists in implementing model-to-model transformations using Domain Specific Languages inspired by ATL [START_REF] Jouault | ATL: A model transformation tool[END_REF] targeting the BIP model and comparing their expressiveness with our approach. the local pointcut expression (a ∈ select g (C, gpc)). According to Proposition 1, any interaction a ∈ select g (C, gpc) is a joinpoint, specifically a = rem g (a, F b , F a ).

PROOF (OF PROPOSITION 3)

. Let e = l, v , τ, l , v , we assume that lpc does not contain portEnabled(p). The proof follows by induction on the structure of lpc. PROOF (OF PROPOSITION 4). We consider F b and F a to be the advice before and after update functions, and the local event e i ∈ T k and e = rem k (e i , F b , F a ) to be the constructed event without the advice. The proof is split into two parts: the first proves the correct application of an advice's update functions, the second proves the correct application of reset locations.

. (e i = ∧ e i lpc) iff before(e i , F b , d) ∧ after(e i , F a , d)

We distinguish two cases based on early(lpc).

Case 1: early(lpc) = false. This case includes the edit frames CB , CE , RUN , CE . before(e i , F b , false) ∧ after(e i , F a , false) simplifies to ∃F : e i .τ.func = F b , F, F a .

Case 1.1. We consider that portEnabled is not included in lpc, then the advice is woven on the update function F , e i .τ = , p, g, F b F F set F a , iff it is the result of a matching transition ∃t : t = , p, g, F, ∈ M according to wframe cur in Definition 24 with e i .τ ∈ m(t). We have t = rem k (e i , F b , F a ).τ and t ∈ select (B k , lpc) iff rem(e i , F b , F a ) lpc from Proposition 3. Case 1.2. We consider that portEnabled is included in lpc, the set of enabled ports in the expression is P = sp(lpc). Using the definition of wframe runa in Definition 24, the advice is woven on the transition e i .τ = , p, b aop ∧ g, F b , F, F a , iff ∃t : e i .τ ∈ m(t) with t = , p, g, F, = rem k (e i , F b , F a ).τ . We decompose rem k (e i , F b , F a ) lpc into two conditions rem k (e i , F b , F a ) c 1 ∧ rem k (e i , F b , F a ) c 2 , where c 1 contains the conjunction of all the portEnabled pointcuts and c 2 contains all the rest (as per Definition 19).

1. e i .τ ∈ select (B k , lpc) iff e i c 2 by applying Proposition 3 to the syntactic part.

2. e i .τ executed iff b aop is true. b aop is true iff mkGuard(P, , M ) since the instrumentation guarantees that the only transitions that set b aop are guarded by mkGuard. M contains all the transitions outbound from since portEnabled uses siblings (Definition 20). However, by the definition of mkGuard, mkGuard iff ∀p j ∈ P, ∃ rem k (e i , F b , F a ).l : p j , g j , f j , j with g j (rem k (e i , F b , F a ).v) = true. Therefore, mkGuard iff e i c 1 .

Therefore, we have:

before(e i , F b , false) ∧ after(e i , F a , false) iff e i = ∧ e i lpc Case 2: early(lpc) = true. This case includes the edit frames PE , CB , RUN , CB . before(e i , F b , true) ∧ after(e i , F a , true) simplifies to ∃F, F : e i-1 .τ.func = F, F b ∧ e i .τ.func = F a , F . The proof is similar to Case 1, we assume i > 0 for simplicity and decompose into two cases: lpc does not contain (resp. contains) portEnabled and use the definition of wframe prev and wframe runb from Definition 24 respectively. e i .τ corresponds to a t ∈ M . Since we consider the event before e i1 .τ we note that both frames weave on all transitions that lead to M . In the case of wframe prev , F b is woven at the end of all transitions in P (M ) \ M and in the case of the loop from the created locations to the locations from which M is outbound therefore including all possible previous transitions. In the case of wframe runb , F b is woven at the created transition guarded by mkGuard (which is true).

. (e i = ∧ e i lpc) =⇒ (R = ∅ =⇒ ∃r ∈ R : reset(e i , r)

Since it is possible to constructs e i and e i is a joinpoint, we decompose e i lpc = e i c 1 ∧ e i c 2 into a conjunction of two conditions (similarly to Case 1.2). c 1 is a conjunction of all portEnabled pointcuts and c 2 all the rest.

1. Since e i c 1 , we have ∀p j ∈ sp(lpc) : ∃τ = e i .l, p j , g τ , f τ , τ by Definition 19 with e i .τ ∈ siblings(τ ) (definition of siblings). Therefore, e i .τ ∈ select (B k , c 1 )

2. From Proposition 3, e i c 2 iff e i .τ ∈ select (B k , c 2 ).

We have from the above e i .τ ∈ select (B k , c 1 ) ∧ e i .τ ∈ select (B k , c 2 ) iff e .τ ∈ (select (B k , c 1 ) ∩ select (B k , c 2 )).

Definition 4 (

 4 trans such that:[START_REF] Aksit | An object-oriented language-database integration model: The composition-filters approach[END_REF] the guard before receiving the new valuation v p of the port variables holds, i.e., g τ (v) = true, and (2) the application of the update function F τ (v p /v) yields v . A transition is labeled with port along with valuation of its variables v p , which is possibly received from other components. Semantics of an atomic component). The semantics of an atomic component B is the LTS S B = B .locs × X, B .ports × X, → , where:

Figure 1 :

 1 Figure 1: Two communicating agents

  Account ----+ getOwner() : User ---S + getBalance() : Dollars PL-S + deposit(amt : Dollars) PL-S + withdraw(amt : Dollars) AccountController PL-S + wire(from : Account, to : Account, amt : Dollars) : bool PL-S + close(acct : Account) : bool PL-S + open(user : User, balance : Dollars) : Account -LC-+ list(user : User) : Account[ ] UserController PL-S + create(data : UserData) : User --C-+ get(code : Integer) : User --C-+ find(name : String) : User[ ] PL-S + block(user : User) : bool User --CS + getInfo() : UserData ----+ getCode() : Integer -L--+ getLastActivity() : Date P: Persistence L: Logging C: Caching S: Security Policy

Figure 2 :

 2 Figure 2: Multiple concerns in a simple system

Figure 3 :

 3 Figure 3: Matching and Weaving a Global Aspect

Example 8 (

 8 Adding an inter-type component to a model).

  Figure 3b depicts π(γ(B ∪ {B V })) where V = {v 0 , v 1 } and C = π(γ(B)). A new atomic component B V is created. B V has the variables v 0 and v 1 and has its port p V always enabled. The variables in V are attached to p V . Weaving the advice. Once the inter-type component is added to the model, the advice is woven by connecting the existing interactions to it. Definition 18 (Global weave). Given a composite component C = π(γ(B)), a set of interactions I, the set of inter-type variables V , and a global advice adv = F b , F a , the global weave is defined as C = weave g (C, I, V, adv) where

Listing 2 :

 2 Local Pointcut Expression lpc : lpc 'and' lpc | atom; atom : 'atLocation' '(' ')'

A

  local pointcut expression selects local joinpoints. Considering the multitude of joinpoints, we use a grammar for specifying the pointcut expression, which makes it more readable and easier to combine. Pointcut expressions are defined using the grammar in Listing 2, where ∈ B k .locs, x ∈ B k .vars, p ∈ B k .ports. Definition 19 (Matching of a local joinpoint with a local pointcut expression). A local joinpoint e matches the pointcut expression lpc, noted e lpc, iff match lpc with | φ and φ → e φ ∧ e φ | atLocation( ) → (e.l = ) | readVarGuard(x) → (∃t ∈ B k .trans : t.src = e.l ∧ x ∈ readguard(t)) | readVarFunc(x) → (x ∈ readvar(e.τ.func)) | write(x) → (x ∈ writevar(e.τ.func)) | portEnabled(p)

Figure 4 :

 4 Figure 4: Syntax Representations

  Figure4aillustrates origin(M ), dest(M ), siblings(M ) and prev(M ). The origin set contains the locations from which the transitions in M are outbound: { 0 , 2 }. The destination set contains the locations to which the transitions in M lead to: { 1 , 4 }, and are highlighted with a pattern. The dotted transitions belong to siblings(M ), they are all transitions originating from origin(M ) i.e.,

Figure 5 :

 5 Figure 5: Matching Ports

  A local advice ladv(B k , V ) is a triple F b , F a , R . It has access to X adv = B k .vars ∪ V . It consists of: 1. a before function F b such that (readvar(F b ) ∪ writevar(F b )) ⊆ X adv ;

Figure 6 :

 6 Figure 6: Weaving Reset Locations

Figure 7 :

 7 Figure 7: Weaving RUN , CB

Proposition 4 .

 4 Correctness of local advice weaving. Consider T to be the sequence of global events of the BIP System C , Q 0 where C = C B k , lpc, V, ladv(B k , V ) and B k is the new atomic component with F b and F a as the advice before and after update functions. Let T k = map(T , B k ) = (e 0 • e 1 • . . .), d = early(lpc), we have ∀e i ∈ T k , e i = rem k (e i , F b , F a ):

Figure 8 :

 8 Figure 8: Weave Procedures

Figure 9 :

 9 Figure 9: Reset Location Interference

[Figure 10 :

 10 Figure 10: The Network Component

Figure 11 :

 11 Figure 11: Authentication aspects and resulting execution. The aspects extends the behavior by verifying a hash of the messages and forwarding or blocking the message.

e

  lpc iff τ ∈ select (B k , lpc)Base cases:e atLocation( ) iff l = (Definition 19) iff τ.src = iff τ ∈ {t ∈ B k .trans | t.src = } iff τ ∈ select (B k , atLocation( )) (Definition 20) e readVarGuard(x) iff (∃t ∈ B k .trans : t.src = l = τ.src ∧ x ∈ readguard(t)) (Definition[START_REF] Duclos | Describing and using non functional aspects in component based applications[END_REF]

  iff τ ∈ siblings(t) (Def. siblings)iff τ ∈ select (B k , readVarGuard(x)) (Definition 20) e readVarFunc(x) iff (x ∈ readvar(τ.func)) (Definition 19) iff τ ∈ {t ∈ B k .trans | x ∈ readvar(t.func)} iff τ ∈ select (B k , readVarFunc(x)) (Definition 20) e portExecute(p) iff (τ.port = p)) (Definition 19) iff τ ∈ {t ∈ B k .trans | t.port = p} iff τ ∈ select (B k , portExecute(x)) (Definition 20)e write(x) iff τ ∈ select (B k , write(x)) is shown by replacing in the above: readVarFunc(x) with write(x).Inductive step: e φ and φ iff e φ ∧ e φiff τ ∈ select (B k , φ) ∧ τ ∈ select (B k , φ )(Hypothesis)iff τ ∈ select (B k , φ) ∩ select (B k , φ )

Table 1 :

 1 Traces According to Views

Table 2 :

 2 Crosscutting concerns in Network

	# Concern	Transitions Interactions OT	OI	OC
	1 Logging	10	0	5	0	2,3
	2 Authentication	2	1	2	1	1,3.4
	3 Congestion	5	0	4	0	1,2
	4 Fault Tolerance	0	3	0	1	2
	Network	12	5

Similarly, in a regular program, adding extra code before a function call at the source-code level, results in executing the code before the function call during the execution of the program. However, we note that this is not as straightforward for the semantics of BIP.

The full grammar can be found in Appendix B.

We chose to use Aspect instead of Container as an implementation decision to have a similar notion than that of AspectJ, since AspectJ defines multiple pairs of pointcut and advice to be an aspect.

Acknowledgment

The authors acknowledge the support of the ICT COST (European Cooperation in Science and Technology) Action IC1402 Runtime Verification beyond Monitoring (ARVI) and the University Research Board (URB) at American University of Beirut.

They contain the advices necessary to implement a crosscutting concern. Interaction with the advice happens through additional interfaces called advice interfaces. Moreover, aspects components expose regular interfaces. Thus, they can be seen as regular components. Joinpoints are a combination of interfaces of different components. Thus, components are seen as black boxes. The interception model is based on composition filters [START_REF] Aksit | An object-oriented language-database integration model: The composition-filters approach[END_REF] extended from objects to components. The model is mapped onto Fractal, a modular and extensible component model [START_REF] Bruneton | An open component model and its support in Java[END_REF]. This approach has several advantages. First it explicitly models dependencies between aspects and components, and allows for their composition at an architectural level. Second, it allows the aspects to be manipulated and reconfigured at runtime. Third, it clearly defines the relationships (1) between aspects and other aspects, and (2) between aspects and the components they modify. This approach, however, does not consider the semantics of interactions. It targets arbitrary interface signatures, so the implementation itself must explicitly address the synchronization amongst the different components and data transfer. Notions of before, after differ from just executing a function. In the simplest case, a BIP interaction requires ports to be all enabled, therefore before

Appendix A. Proofs

The common assumption for the proofs that include the advice F b and F a functions, is that F b and F a can be uniquely determined and are not empty. To ensure this, one can add code markers at the start and end of each F b and F a which have no effect and are not present in the original system. PROOF (OF PROPOSITION 1). We consider a global event q, a, q ∈ E and a global pointcut expression p, v r , v w . The proof follows from the definition of select g (C, gpc) which selects all interactions matching the criteria that should be matched by (E i = q, a, q gpc).

(a p, v r , v w ) iff p ⊆ a.ports

PROOF (OF PROPOSITION 2). Given a global advice F b , F a . We consider an executed interaction a ∈ E , and rem g (a, F b , F a ) = a the constructed interaction without the advice.

An executed interaction's update function a.func starts with F b and ends with F a , according to the definition of m() in Definition 18 iff it is the result of weaving the advice on it from an interaction a (∃a ∈ γ : m(a ) = a ∧ a ∈ I). The interaction a is in I iff it was selected by Therefore e i lpc iff e i .τ ∈ select (B k , lpc) (i.e., e i .τ ∈ M and e i .τ ∈ m(e i .τ )). The local weave guarantees that since e i .τ ∈ M then F set has been called either on e i .τ in the case where portEnabled is not present, or e i-1 .τ (F set is in the update function of the created transition precedes e i .τ guarded by mkGuard). The local weaving (Definition 24) ensures for all cases of edit frames, that the transitions will lead to a location on which reset location is woven (by using dest(M ) and adding the appropriate created locations). Therefore, it ensures that the next location after e i .τ executes, contains all reset location pairs if R = 0. Using the definition of wReset (Definition 24), for any r j = g j , dest j ∈ R, we have a transition reset j = e i+1 .l, ip, b aop ∧ g j , f j , dest j . The port ip corresponds to an interaction with the highest priority, therefore if ip is enabled, i.e., b aop ∧ g j (e i+1 .v) then it will execute with higher priority than other transitions on the location. Since b aop = true, if g i (e i+1 ) then the component will execute the reset location transition and move to dest j (i.e., e i+1 .l = dest j ).

Appendix B. AOP-BIP Language

The AOP-BIP language (overviewed in Section 8.1) follows the ideas presented in this paper. Because of the differences between the global and the local view, the grammar distinguishes global from local pointcut expressions and advices. Furthermore, the identifiers specified in the AOP model generated from an .abip file are expected to reference identifiers in the BIP model generated from the .bip file. The validators modules (both local and global) in the tool are responsible for verifying that the identifiers match.