Alexander Graf-Brill

Holger Hermanns

Component-aware Input-Output Conformance

Keywords: Model-based testing, Input-output conformance, Compositionality

Black-box conformance testing based on a compositional model of the intended behaviour is a very attractive approach to validate the correctness of an implementation. In this context, input-output conformance is a scientifically well-established formalisation of the testing process. This paper discusses peculiar problems arising in situations where the implementation is a monolithic black box, for instance for reasons of intellectual property restrictions, while the specification is compositional. In essence, tests need to be enabled to observe progress in individual specification-level components. For that, we will reconsider input-output conformance so that it can faithfully deal with such situations. Refined notions of quiescence play a central role in a proper treatment of the problem. We focus on the scenario of parallel components with fully asynchronous communication covering very many notorious practical examples. We finally illustrate the practical implications of component-aware conformance testing in the context of a prominent example, namely networked embedded software.

Introduction

Component-based or modular systems are systems which are composed of several components in order to provide a higher degree of functionality or just to offer the ensemble of features offered by its components. From an implementation point of view, component-based systems are very flexible since single components can be updated or exchanged easily, or the system can be extended by additional components, without having to touch the whole system.

When it comes to the verification of such systems, one usually tries to benefit from the compositional structure. Correctness of the components is easier to verify in isolation and under appropriate conditions, correctness of the whole system is derived from the correctness of all components. This reduces the overall verification effort. In particular, when updating a single component of the system, one only has to verify the new component without the need to verify the other components again. However, this approach is only applicable if the correctness properties are compositional [START_REF] Graf | Compositional minimisation of finite state systems using interface specifications[END_REF][START_REF] Garavel | Compositional verification of asynchronous concurrent systems using CADP[END_REF][START_REF] Henzinger | You assume, we guarantee: Methodology and case studies[END_REF][START_REF] Van Der Bijl | Compositional testing with ioco[END_REF][START_REF] Janssen | Matching Implementations to Specifications: The Corner Cases of ioco[END_REF][START_REF] Noroozi | Decomposability in input output conformance testing[END_REF][START_REF] Benes | Complete composition operators for ioco-testing theory[END_REF].

Model-based testing is a validation technique where, based on a formal specification of a system, a suitable set of experiments (test suite) is generated in an automated manner and executed on the implementation of that system, so as to assert some notion of conformance between the implementation and its specification. In model-based testing, compositional testing is a research area of its own. Given a specification and an implementation under test (IUT), each as combinations of several components, a compositional conformance tester checks conformance between the components of the specification and the respective IUT components, so as to conclude conformance between the combined specification and IUT. If this implication holds, there is no need for further integration testing when combining the different IUT components [START_REF] Van Der Bijl | Compositional testing with ioco[END_REF]7,[START_REF] Gotzhein | Compositional testing of communication systems[END_REF][START_REF] Carver | A modular approach to model-based testing of concurrent programs[END_REF]3]. Otherwise this is a costly and time-consuming step since the combined specification has to be taken into account which is notorious in size relative to the sizes of the individual components.

What all these approaches have obviously in common is the assumption that the IUT is indeed a combination of several components which can be accessed individually. Interestingly little attention has been payed to the situation where only the specification is composed of clearly distinguished components, but the IUT is a single black box, i.e. a monolithic object, or an object where components are not accessible in isolation.

We consider this as a mismatch, since the previously described scenario is pretty much the norm for black-box systems protected by intellectual property rights. Especially if such systems need to undergo a certification according to some well-structured component-based or scenario-based standard. This is the concrete problem motivating our work. But beyond that there are several other reasons for attacking this challenge.

Since there are no dedicated theoretical approaches targeting the testing of such scenarios, the standard input-output conformance [START_REF] Tretmans | Model based testing with labelled transition systems[END_REF] is the natural base methodology. Input-output conformance (ioco) is based on the idea that a reasonable implementation of a formally specified system should assure that the IUT progresses as foreseen by the specification, and this progress is observable by the tester.

Since IUT progress corresponds to outputs of the IUT, this means that 1. any interaction sequence between tester and IUT possible according to the specification is followed only by IUT outputs foreseen according to the specification; 2. only in situations where no IUT output is foreseen, the IUT is allowed to be quiescent.

Quiescence, and especially the possibility to observe quiescence is a crucial ingredient to the theory of input-output conformance. It makes progress observable by refining classical testing equivalences and preorders [START_REF] De Nicola | Testing equivalences for processes[END_REF]8] with concepts of refusal testing [START_REF] Phillips | Refusal testing[END_REF][START_REF] Langerak | A testing theory for LOTOS using deadlock detection[END_REF], thus enabling a more fine grained relation between systems based on their state-based capabilities to produce any output at all. In practice, quiescence is approximated by timeout mechanisms: If after some interaction sequence no IUT output is witnessed before the timeout, the IUT is interpreted as now being quiescent. The concept of quiescence therefore provides an implicit mechanism to test for absence as well as presence of progress, without an explicit reference to real time. This paper explores the simple question what needs to change in the theory of input-output conformance in order to be able to test for the progress of components of a component-based specification. So, we add the idea that a reasonable implementation of a component-based system should assure that the IUT progresses as foreseen by the component-based specification, and this progress is observable by the tester. This then translates concretely to (the first item being unchanged), 1. any interaction sequence between tester and IUT possible according to the specification is followed only by IUT outputs foreseen according to the specification; 2. only in situations where no IUT output is foreseen by some component, the IUT is allowed to be quiescent with respect to that component.

The first requirement is indeed the standard ioco criterion considering functional correctness of an IUT. The second requirement is the core motivation for this paper. This requirement harvests the available information about the inner structure of a compositional specification. Since the specification is white-box, any observable behaviour of the system can be associated to the components possibly causing that behaviour. This provides the opportunity to deduce which components are taking part in an interaction, and effectively enables a finegrained notion of quiescence. With this, we require an IUT to progress whenever possible not only on the system-level, but instead for each component of a composed system. Notably, we will apply this to monolithic black-box implementations, but we nevertheless ask them to respect the compositional nature of their specification. From a testing perspective this implies among others that we would reject an implementation which only exhibits the behaviour of a single component, in situations where other components can not stay quiescent i.e. they potentially can progress by observable behaviour. We make all this deducible by only looking at the compositional specification.

Organisation of the paper. After setting the stage, we first argue why precisely standard input-output conformance is ill-suited for the problem at hand. We then focus on specifications that are fully asynchronous, so they are merely collections of behaviour descriptions where none of the behaviour emerges through interaction across components. This is a very widespread scenario in practice. We explain the details of a natural solution which comes with adaptations to the quiescence definition. On the practical side we discuss in how far the resulting notions can indeed be tested for, which leads to a well-motivated revision of the theory. We finally illustrate the practical implications of component-aware conformance testing in the context of networked embedded software.

Preliminaries

The basis for model-based testing is a precise specification of the IUT which unambiguously describes what an implementation may do, respectively not do.

Input-output transition systems. A common semantic model to describe the behaviour of a system are labeled transition systems (LTS). In the presence of inputs and outputs, a suitable variation is provided by Input-Output Transition Systems (IOTS). Definition 1. An input-output transition system is a 5-tuple Q, L ? , L ! , T, q 0 where -Q is a finite, non-empty set of states; -L ? and L ! are disjoint countable sets (L ? ∩ L ! = ∅) of input labels and output labels, respectively;

-T ⊆ Q × (L ∪ {τ }) × Q, with τ /
∈ L, is the transition relation, where L = L ? ∪ L ! ; -q 0 is the initial state.

The class of input-output transition systems with inputs in L ? and outputs in L ! is denoted by IOT S(L ? , L ! ).

As usual, τ represents an unobservable internal action of the system. We write q µ -→ q if there is a transition labelled µ from state q to state q , i.e., (q, µ, q ) ∈ T . The composition of transitions q 1 µ1•µ2•...•µn-1 ----------→ q n expresses that the system, when in state q 1 , may end in state q n , after performing the sequence of actions µ 1 • µ 2 • . . . • µ n-1 , i.e. ∃(q i , µ i , q i+1 ) ∈ T, i ≤ n -1. Due to nondeterminism, it may be the case, that after performing the same sequence, the system may end in another state (or multiple such states):

q 1 µ1•µ2•...•µn-1 ----------→ q n with q n = q n .
Traces and derived notions. Usually an IOTS can represent the entire behaviour of a system, including concrete interactions between system and environment. One such behaviour is represented by a so-called trace, of which we are only interested in its observable part, obtained by abstracting from internal actions of the system. Let p = Q, L ? , L ! , T, q 0 be an IOTS with q, q ∈ Q, L = L ? ∪L ! , a, a i ∈ L, and σ ∈ L * . We write q =⇒ q to express that q = q or q τ

•••••τ ----→ q . q a =⇒ q denotes the fact that ∃q 1 , q 2 ∈ Q : q =⇒ q 1 a -→ q 2 =⇒
q . This can be extended for a sequence of actions q a1•...•an = ==== ⇒ q s.t. ∃q 0 , ..., q n ∈ Q : q = q 0 a1 =⇒ q 1 a2 =⇒ . . . an =⇒ q n = q . q σ =⇒ and q σ =⇒ are then defined as ∃q : q σ =⇒ q and q : q σ =⇒ q , respectively. Furthermore, init(q) denotes the set of available transitions in a state q, i.e., {µ ∈ L ∪ {τ } | q µ -→}. The set of traces starting in state q is defined as traces(q) = def {σ ∈ L * | q σ =⇒}. For a given trace σ, the set of reachable states is given by the definition q after σ = def {q | q σ =⇒ q }. The extension for starting in a set of states Q is Q after σ = def {q after σ | q ∈ Q }. With der (q) we denote the set of all reachable states from q, i.e., {q | ∃σ ∈ L * : q σ =⇒ q }. Following the standard literature, we restrict ourselves to strongly convergent IOTS i.e. there is no state that can perform an infinite sequence of internal transitions. An IOTS p is called input-enabled, if and only if all its reachable states q are input-enabled i.e. ∀q ∈ der (p), ∀a ∈ L ? .q a =⇒. So, inputs can never be blocked (or come as surprises). It is common practice to work with specifications modelled as IOTS without requiring input-enabledness while IUTs are required to be represented as input-enabled IOTS. This is what we assume here, too.

Input-output conformance and quiescence. A specific conformance relation, inputout conformance (ioco) [START_REF] Tretmans | Model based testing with labelled transition systems[END_REF] dominates theoretical as well as practical work on model-based testing. It relates implementations with specifications with respect to the possible output behaviour observed after executing traces of the specification. In ioco, the output behaviour includes a designated output quiescence, abbreviated with the special label δ. Quiescence represents the situation when there is no output to observe at all. A state q is said to be quiescent, denoted by δ(q), iff init(q) ∩ (L ! ∪ {τ }) = ∅.

Assuming δ / ∈ (L ∪ {τ }) it is technically convenient to encode quiescence wherever present into the transition structure at hand. For this a suspension automaton ∆(p) is constructed out of an IOTS p, where transitions q δ -→ q are added to any quiescent state. The set of possible outputs of a state q is then defined as out(q) = def {a ∈ L ! | q a -→} ∪ {δ | δ(q)}, and this is lifted to sets of states P by out(P ) = def {out(q) | q ∈ P }. Since quiescence is now interpreted as an additional observable output, we extend the definition for traces to suspension traces. Definition 2. Let p = Q, L ? , L ! , T, q 0 ∈ IOT S(L ? , L ! ). The suspension traces of p are given by Straces(p)

= def {σ ∈ (L ∪ {δ}) * | q 0 σ =⇒}.
The definition of ioco then looks as follows:

Definition 3. Given a set of input labels L ? and a set of output labels L ! , the relation ioco ⊆ IOT S(L ? , L ! ) × IOT S(L ? , L ! ) is defined for a specification s and an input-enabled implementation i as i ioco s ⇔ def ∀σ ∈ Straces(s) : out(i after σ) ⊆ out(s after σ) Partial specifications. Since ioco is defined based on the suspension traces of the specification on the one hand, and only requires inclusion of the output behaviour of the IUT w.r.t. the specified outputs on the other hand, it is possible to have partial specifications. This means that an IUT does not have to implement all specified output transitions of a certain state, but these can be seen as output alternatives. Furthermore, there are no restrictions on the behaviour of an implementation once its execution left the suspension traces of the specifications i.e. it performs an underspecified trace. Since an underspecified trace always starts with an unspecified input action for a state input-enabled specifications do not have any underspecified trace.

Test generation and execution. Theoretically, a test case is a variant of an IOTS with two special trap states labeled pass and fail, whereby each other state represents all states of the specification which are reachable by the suspension trace corresponding to the trace that leads to this particular state of the test case. In order to detect quiescence, the special transition label θ is used in order to synchronise with δ. A test case is then generated based on the definition of ioco in an iterative manner. In each iteration step there are three options. 1) For all outputs in L ! and quiescence a correspondingly labelled transition is added. If the output is not foreseen by the specification, the successor state is the special state fail and for all valid successor states the test case generation algorithm continues in the next iteration step. 2) An input action which is enabled in one of the encoded states of the specification is chosen and a correspondingly labeled transition is added to the test case. In order to handle interrupting outputs of the IUT, corresponding transitions are added as described in 1). 3) At any iteration step, the algorithm can be stopped by placing the special state pass.

An execution of a test case is then the parallel composition of the test case and the IUT. A test run is any trace of the parallel composition which ends in a state which is labeled with pass or fail. An IUT passes a test case if and only if all possible test runs lead to states labeled with pass. It fails the test case otherwise. By assuming some kind of fairness, an IUT will reveal sooner or later all its nondeterministic behaviour when repeatedly executed with a test case.

From a practical point of view, quiescence detection is realised by introducing a timer. This timer is restarted after every interaction with the IUT and upon its expiration, quiescence of the implementation is assumed and accordingly processed.

Before we delve deeper into conformance testing of component-based systems, we first give a formal definition of what we actually understand of a componentbased system. Definition 4. A component-based input-output transition system (CIOTS) is a 6-tuple Q, L ? , L ! , T, q 0 , C where the system is the composition of components in the non-empty vector

C = s 0 , . . . , s n with n ∈ N 0 -each s k ∈ C is a finite input-output transition system Q k , L ?k , L !k , T k , q 0,k ∈ IOT S(L ?k , L !k ) -all components are pairwise action-disjoint i.e. ∀s k .L ?k ∩ sm∈C L !m = ∅ ∧ L !k ∩ sm∈C L ?m = ∅ -the
sets of input labels and output labels are

L ? = s k ∈C L ?k and L ! = s k ∈C L !k -the set of states Q is the cross product of the set of states of the components in C, i.e. Q = s k ∈C Q k -the initial
state q 0 is the cross product of the initial states of the components in C, i.e. q 0 = s k ∈C q k,0 the transition relation T is the combination of the transition relations of the components s.t. The class of component-based input-output transition systems with inputs in L ? and outputs in L ! is denoted by CIOT S(L ? , L ! ). We say that a system s is component-based, if and only if, s ∈ CIOT S(L ? , L ! ) for some L ? and L ! .

T = {(q 0 , . . . , qk , . . . , qn ) µ -→ (q 0 , . . . , q k , . . . , qn ) | qk µ -→ q k ∈ T k } b1 sig 1 ! (a) Component ∆(b) g1 g2 strt? δ stp? sig 2 ! (b) Component ∆(g) s1,1 s1,2 sig 1 ! strt? stp? sig 1 ! sig 2 ! (c) Composition ∆( b, g )
Notably, Q, L ? , L ! , T, q 0 is itself a finite input-output transition system in IOT S(L ? , L ! ). Since a CIOTS is already completely defined by its components, we may use the abbreviation s 0 , . . . , s n in order to refer to s = Q, L ? , L ! , T, q 0 , s 0 , . . . , s n .

Example 1. In Figure 1 a very simple component-based specification is displayed. Figure 1a and Figure 1b show the suspension automata of the IOTSs of components b and g, each specifying some kind of sensor. Sensor b can be thought of as continuously gathering some measurement data (not modelled) which it passes on to the environment via the action sig 1 !. Sensor g works similarly using action sig 2 !, but can be started (strt? ) and stopped (stp? ) from remote. Initially it is stopped -and hence quiescent.

Each IOTS s = Q, L ? , L ! , T, q 0 can be represented as a single-component CIOTS ŝ = Q, L ? , L ! , T, q 0 , s and vice versa.

Conformance and component behaviour

This section provides a motivation why the well-established general ioco testing procedure falls short when facing a component-based specification w.r.t. the conditions we postulated in Section 1.

i 1 sig 1 ! strt?
stp? Example 2. A potential candidate implementation i of the composed specification from Figure 1 is displayed on the right. It is input-enabled (w.r.t. the set {strt?,stp? }). Indeed, this implementation does conform to the specification, i.e. i ioco b, g , since ∀σ ∈ Straces(i) : out(i 1 after σ) = {sig 1 !} and ∀σ ∈ Straces( b, g ) : out(s 1,1 after σ ) is either

{sig 1 !} or {sig 1 !, sig 2 !}.
Notably, implementation i does never offer the output action sig 2 !, so the core behaviour of sensor g is effectively not present in the implementation. While this omission of behaviour is perfectly legal for the theory of ioco, we feel that such an implementation does not exhibit the intended behaviour of two sensor nodes being combined as specified above. According to our initial reasoning, after providing the input strt? it is not foreseen by component g to produce no output, thus implementation i is not allowed to be quiescent w.r.t. component g.

One may object that, of course, a good compositional testing procedure should preferably be based on tests of individual components in case they do not interact with each other. Therefore one would a priori require that i ioco b as well as i ioco g. Indeed, it turns out that i ioco g (due to the presence of the output action sig 1 !, which is not foreseen by g) while i ioco b. So, from this perspective, the implementation i is not entirely convincing as a witness for the shortcoming of the classical ioco theory.

j 1 j 2 sig 1 ! stp? strt? stp? sig 2 ! strt?
Example 3. Another implementation candidate j is displayed on the right. It correctly outputs sig 1 ! in the initial state and starts and stops producing the output sig 2 ! as intended by the inputs strt? and stp?. However, the output sig 1 ! is turned off in state j 2 where the output sig 2 ! is produced only. Again it holds that j ioco b, g .

The essence of the problem of implementation j is similar to the one of i appearing in Example 2. Contrary to what we assume reasonable, some valuable output behaviour of the specification of component b is not implemented, but here this is in a fragment of the state space reachable by transitions belonging to specification of component g. In this example, j ioco b as well as j ioco g provided we assume a suitable projection mechanism to filter the observable behaviour corresponding to the component under test.

As it stands, focusing on the behaviour of a single component, is no solution in a quest for a compositional testing theory. Instead one has to foresee arbitrary input actions of other components, in order to examine the full behaviour of an IUT. Unfortunately, "the full behaviour of an IUT" might include underspecified behaviour in case of specifications that are not input-enabled (which is not uncommon). This in turn might lead to outputs interfering with our current test run, thus, rendering such a testing approach useless, again. Hence, one has to adjust the provided inputs to the behaviour of the composed specification.

For now, we can conclude that the standard ioco approach is not well suited for testing scenarios involving compositional specifications. The problem is twofold. On the one hand, ioco is not aware of the underlying topology of the specification model. On the other hand, the relation is based on excluding unspecified output behaviour, rather than enforcing a certain output (set). We shall see that the concept of quiescence is the central leverage point regarding both aspects of the problem.

A component-aware theory

The lesson learned in the previous section is that the ioco approach fails at considering simultaneously the specific output behaviour of the individual components embedded in the overall behaviour of a composed specification. Especially the absence of any output from a particular component can not be detected. This is however the only indicator at hand whether or not a specified component does take part in the interactions of the IUT, or not. Thus, a quiescence definition based on the output capabilities of single components is needed.

The composition setting has similarities to the multi-ioco (mioco) relation as presented in [START_REF] Heerink | Ins and Outs in Refusal Testing[END_REF] where communication with a system is assumed to occur on multiple distinct interaction interfaces and quiescence is then redefined s.t. each interface is associated with a dedicated quiescence action. No component structure is considered, implying that this approach is not applicable rightaway to the problem we consider. However, it serves as a strong inspriation for our approach, in which we will indeed customise the definition of mioco to our componentbased setting. To get started, we assume an indexed family of quiescence labels of the form δ k for k ∈ N. These will serve as means to signify quiescence per individual component. Definition 5. Let p = (p 0 , . . . , p n ) be a state and P be a set of states of a CIOTS s = Q, L ? , L ! , T, q 0 , C ∈ CIOT S(L ? , L ! ), where C = s 0 , . . . , s n is the finite, non-empty set of component IOTS s k = Q k , L ?k , L !k , T k , q 0,k . We define a vector δ (of dimension n) of quiescence labels by setting

δk (p) = def δ(p k ) for 0 ≤ k ≤ n (1)
and we propagate this into the other elements of the theory by redefining

-out(p) = def {x ∈ L ! | p x -→} ∪ {δ k | δk (p)}, -∆(s) = Q, L ? , L ! ∪ {δ k | 0 ≤ k ≤ n}, T ∪ {p δ k -→ p | p ∈ Q, δk (p)}, q 0 , C , -Straces(s) = def {σ ∈ (L ∪ {δ k | 0 ≤ k ≤ n}) * | ∆(s) σ =⇒}.
Definition 5 provides a component-specific version of quiescence and redefines out() and Straces() w.r.t. this quiescence definition, where the latter one is based on the corresponding redefinition for the suspension automaton ∆(s) of a CI-OTS s.

The behaviour of an IUT is to be interpreted relative to a given specification CIOTS, which in essence means that the output alphabets of that CIOTS induce vectors of quiescence labels for the IOTS representing the IUT, too. But since IUTs are no CIOTSs themselves, the quiescence notion δ from Definition 5 can not be applied directly. Thus, we need a quiescence definition and a corresponding definition of the suspension automaton for input-enabled IOTSs, given the output alphabets of interest. Definition 6. Let p be a state and P be a set of states of an IOTS s = Q, L ? , L ! , T, q 0 ∈ IOT S(L ? , L ! ), and L = (L !0 , . . . , L !n ) be a finite vector of

≤ k ≤ n, δ L k (p) = def init(p) ∩ (L !k ∪ {τ }) = ∅ (2)
and we propagate this into the definition of the suspension automaton by setting

∆ L (s) = Q, L ? , L ! ∪ {δ k | 0 ≤ k ≤ n}, T ∪ {p δ k -→ p | p ∈ Q, δ L k (p)}, q 0 .
Example 4. We revisit Figure 1 from Example 1. In the presence of Definition 5, the loop g 1 δ -→ g 1 from component g translates to a loop in s 1,1 labeled δ 2 in Figure 1c. This is the only difference. Corresponding to Definition 6, implementation i from Example 2 is quiescent for component g in its initial state and so is implementation j appearing in Example 3. In addition, the latter is quiescent for component b in state j 2 . Thus, their corresponding suspension automata for the vector of output label sets L = ({sig 1 !}, {sig 2 !}) have loops labeled δ 2 at the initial states and δ 1 at j 2 of ∆ L (j). These suspension automata are depicted in Figure 2a and Figure 2b.

For a pair (CIOTS,IOTS) of specification and implementation, Definition 6 will be used on the implementation side and Definition 5 will be used on the specification side. Both are, of course, linked by the vector of output sets L. We assume the component quiescence labels to be uniquely identifiable and consistently chosen throughout the definitions, s.t. indeed the label δ k for a particular output set L !k is identical in each case and matches the quiescence label for the corresponding component s k of the considered CIOTS. This enables us to drop the superscript L . For the remainder of this paper, we are (unless otherwise stated) working with the suspension automata without explicit reference, i.e. we use s and i instead of ∆(s) and ∆(i).

Based on the presented definitions and conventions, the definition for mioco in the context of component-based systems is as follows. Definition 7. Given a set of input labels L ? and a set of output labels L ! , the relation mioco ⊆ IOT S(L ? , L ! ) × CIOT S(L ? , L ! ) for input-enabled implementation i and specification s = Q, L ? , L ! , T, q 0 , C , is defined as follows:

i mioco s ⇔ def ∀σ ∈ Straces(s) : out(i after σ) ⊆ out(s after σ)

Example 5. We check mioco-conformance of the implementation candidates depicted in Figure 2, with respect to the specification displayed in Figure 1. Implementation i does not conform to b, g since out(i after strt?) = {sig 1 !, δ 2 } which is not contained in out( b, g after strt?) = {sig 1 !, sig 2 !}. Likewise, implementation j is rejected again, since state j 2 is quiescent for component b i.e. out(j after strt?) = {sig 2 !, δ 1 }. Contrarily, implementation k mioco b, g , since it implements the missing sig 2 ! transition of implementation j.

A practical theory

When it comes to the practical application of ioco-based testing approaches, the concept of quiescence is implemented by clock timeouts and resets. In the standard ioco setting, a single timer for the system is sufficient. Since mioco is a refinement of ioco one can basically use the standard test generation and execution algorithms [START_REF] Tretmans | Model based testing with labelled transition systems[END_REF], but with additional quiescence timers i.e. one timer per component. The timer for a specific component is then started or reset after each observable interaction with the IUT that belongs to this component, exactly as before when considering a single global component in ioco. This renders ioco testing as a special case of mioco testing. There are however some subtleties in the definition of mioco rooted in the fact that the quiescence definition used for the IUT is state-based.

i 1 i 2 δ 2 y! δ 1
x! Example 6. In Figure 3, we have the specifications of two simple components b and g, always producing the output x! and y!, respectively. Their composition (shown in Figure 3c) is not quiescent for neither of the components. An implementation i which simply alternates between output x! and y! (shown on the right) is quiescent for both components at opposite states, by definition. As a result, i is not mioco-conformal to b, g . However, according to our initial motivation, there is no strong reason why such a system should be rejected. After all it does not produce any unforeseen output (w.r.t. L ! ) and it implements the specified behaviour for both components, by producing x! and y! indefinitely. And in addition, a real physical system would pass any test case that can be generated, provided sufficiently large quiescence timeout values. So we are facing a testing practice that matches our intuition very well, but it does not match the theory. This gap between theory and practice is rooted in the different definition bases for quiescence. Theoretically, conformance is determined by a state-based definition of quiescence. But practical black-box testing does not have information about the internal state of the IUT. As a result, quiescence detection needs to be based on the observed behaviour of the system, i.e. be trace-based. So, what we are after is a fix of the theory on the implementation side, albeit accepting the approximative nature of quiescence being implemented by timers. At the same time we want to maintain the property of our theory refining ioco.

The crux lies in a relaxation δ L k (p) defined in (2) of Definition 6, so that an implementation that postpones outputs of component k for some finite time will not be considered quiescent. Therefore, an IUT will be declared quiescent w.r.t. component k whenever it is quiescent for all components, or it remains silent w.r.t. component k (unless triggered by an input). This intuition is echoed in the following definition.

Definition 8. The relation cioco is defined precisely as the relation mioco in Definition 7, but on the basis of (2) of Definition 6 replaced by

δ L k (p) = def δ(p) ∨ ( ∀σ ∈ traces(p) : σ ∈ (L ! ∪ {τ }) * ⇒ σ ∈ ((L ! \ L !k ) ∪ {τ }) * ∧ τ / ∈ init(p) ) (3)
The last conjunct, enforcing non-quiescence if the implementation can step internally is needed in order to ensure that cioco is a conservative extension of ioco, as we will discuss rightaway. Standard input-output conformances considers states non-quiescent in the presence of outgoing internal transitions on both sides of the relation i.e. specification and implementation.

Example 7. Applying the quiescence notion to implementation i from Example 6 results in a suspension automaton without any quiescent transitions i.e. both states are neither quiescent for component b nor g. Thus, i cioco b, g as intended.

Theorem 1. For specification s ∈ CIOT S(L ? , L ! ), and input-enabled implementation i ∈ IOT S(L ? , L ! ), the following holds:

i cioco s ⇒ i ioco s
A converse result can be established, too: Theorem 2. For action-disjoint specification components s 0 , . . . , s n and inputenabled implementations i 0 , . . . , i n with s k , i k ∈ IOT S(L ?k , L !k ) for 0 ≤ k ≤ n, the following holds:

∀k. i k ioco s k ⇒ i 0 ⊗ . . . ⊗ i n cioco s 0 , . . . , s n
Theorem 1 and Theorem 2 together imply that ioco and cioco are equivalent for single-component specifications.

Example 8. We consider the single component specification b in Figure 4. According to ioco, state b 2 is quiescent while b 1 is not. Therefore the allowed outputs after the traces a? and δa? differ. The same difference applies to the states i 2 and i 1 of the input-enabled IOTS i (because the definition of δ is the same on both sides) and as a result i ioco b holds. The above theorems ensure that i cioco b , too. But Theorem 2 were broken if the conjunct τ / ∈ init(p) were dropped from (3) in Definition 8. In the example, state i 1 would be considered quiescent (for component b), as well, making it indistinguishable from i 2 , while the difference between states b 1 and b 2 would remain, because (1) in Definition 5 reduces to the classic ioco quiescence definition.

So, Theorem 2 hinges on the fact that internal steps are considered nonquiescent in ioco. While this is a useful choice on the specification side [START_REF] Tretmans | Model based testing with labelled transition systems[END_REF], it could be considered a minor shortcoming on the implementation side, where internal steps are simply unobservable. This is rooted in the fact that the same quiescence definition is used on both sides in the standard ioco theory. As far as we are aware, the present work is the first to break with this tradition. If one would do the same for standard ioco, i.e. making internal steps quiescent on the implementation side, the two theorems above could be resurrected on the basis of the following definition replacing (3).

δ L k (p) = def δ(p) ∨ ∀σ ∈ traces(p) : σ ∈ (L ! ∪ {τ }) * ⇒ σ ∈ ((L ! \ L !k ) ∪ {τ }) * (4)
We do not work out the details due to space constraints. Indeed our practical approach works independently of ( 4) and (3) since with blackbox testing in practice no IOTS is given.

Application context EnergyBus. The EnergyBus is a case study [START_REF]CiA 454 Draft Standard Proposal Application profile for energy management systems[END_REF] which drives the concrete development of model-based testing theory and applications of us and our coworkers [START_REF] Graf-Brill | A model-based certification framework for the energybus standard[END_REF][START_REF] Graf-Brill | Modelling and certification for electric mobility[END_REF][START_REF] Graf-Brill | Model-based testing for asynchronous systems[END_REF][START_REF] Marsso | TESTOR: A modular tool for on-thefly conformance test case generation[END_REF]. It aims at establishing a common basis for the interchange and interoperation of electric devices in the context of energy management systems (EMS). The central and innovative role of EnergyBus is the transmission and management of electrical power, in particular the safe access to electricity and its distribution inside an EnergyBus network. Conceptually, EnergyBus extends the CANopen architecture in terms of CANopen application profiles endorsed by the CiA association [START_REF]CiA 301 CANopen Application Layer and Comm. Profile[END_REF]. Among these, the "Pedelec Profile 1" (PP1) is very elaborate, targeting a predominant business context, which is also at the centre of ongoing international standardisation efforts as part of IEC/IS/TC69/JPT61851-3. Alongside with the standardisation, a centralised certification procedure is to be set up, according to some well-structured component-based standard. The specifications themselves are provided as informal combinations of text, protocol flow charts, data tables, and finite state automata (FSA). The definitions include several data structures and various services for e.g. initial configuration, data exchange, and basic communication capability control. The EnergyBus introduces the notion of virtual devices, which encapsulate the functionality of a specific, dedicated role in an EMS, e.g. of a battery pack, a motor, or a sensor unit. A real (physical) device can combine several, not necessarily different, virtual devices. For example, a public charger can be considered as being composed of a voltage converter, a secondary EBC, and a load monitoring unit, each appearing as one virtual device to the protocol. The specification of an EnergyBus-compliant system resembles a hierarchical, tree-like structure as sketched in Figure 5. On top of this schematic structure, technically, a CANopen device might even consist of several EnergyBus devices. A real physical device (field device) might incorporate several CANopen device. The EnergyBus specification is a compositional specification by design. A generic CANopen and EnergyBus device has to deliver several services and continuously transmit contemporary runtime data. Furthermore, depending on the actually implemented virtual device(s), additional services have to be provided. All these protocols are concurrently running and are loosely coupled top-down and horizontally inside of a device. Depending on the chosen degree of abstraction, the involved components are purely asynchronous which holds especially for all device-level abstraction layers.

The theory developed in this paper improves the value of model-based testing in the EnergyBus context to an enormous extent. At the cioco core is a dedicated management of individual timers per specification-level component. The timer for a specific component is started or reset after each observable interaction with the IUT that belongs to this component, just as discussed for mioco in the beginning of Section 5, but now with the matching theoretical underpinning. The concrete difference to the standard, component-unaware testing approach is that the latter is unable to cope with problems as simple as some components just stopping to work. Without our theory extension, these problems induce the need for a careful manual inspection of each seemingly passing test run, in order to double check for the absence of such unwanted behaviour. By using the presented component-aware approach of this paper, all needed checks are done mechanically, on the basis of timer mechanisms that are fully automated.

As an intermediate step, one can use the theory developed to justify a sound transfer of the observation mechanism of the critical circumstances from the tester to the adapter component, sitting between the actual IUT and the tester. The adapter is then equipped with a series of observer processes which maintain dedicated timers for each specific transmission expected from the IUT. The timers are started and stopped, according to the specification knowledge transferred into the adapter component. In case a time-out occurs, the adapter sends a special absenceOfX! output to the tester. Observing that output makes the tester stop with a fail-verdict. Indeed we performed our empirical evaluation succesfully using this approach, too. It however has the drawback that the adapter component needs to be tailored to each case study variation manually. This is not needed if instead implementing the cioco-testing mechanisation as described.

Conclusion

This paper has developed a component-aware, yet conservative, extension of model-based input-output conformance testing. Some effort has gone into making this theory practical, which is linked to asymmetric definitions of component quiescence for specification and implementation.

Our exclusive focus has been on components that do not communicate by synchronisation. However, there are many real world examples where components of a system are meant to exchange information, which is usually modelled by synchronisation over shared or complementary actions. The theory we presented can be extended in this direction, subject to several design choices which for space constraint reasons we can only briefly touch upon here: (1) Synchronisation between components might be internally hidden and its effects may be observable in the behaviour of another component. (2) Component-local progress via synchronisation needs a synchronisation partner which may or may not be available or may preempt a possible synchronisation by alternative transitions. (3) While the standard ioco theory prohibits internal transition cycles, these arise rather natural when considering synchronising components. (4) From a practical point of view, this extended scenario introduces several additional challenges because a timer reset does no longer directly correlate with observable behaviour of a single component.

Figure 1 :

 1 Figure 1: A simple component-based sensor node example.

Figure 2 :

 2 Figure 2: Component-based testing with mioco

Figure 3 :

 3 Figure 3: Non-deterministic encoding of parallel component behaviour.

Figure 4 :

 4 Figure 4: Single components considered with ioco vs. cioco.

Figure 5 :

 5 Figure 5: Schematic view on the specification of an EnergyBus (EB) device

Acknowledgements. This work has received financial support by the ERC Advanced Investigators Grant 695614 (POWVER) and by the Deutsche Forschungsgemeinschaft (DFG, German Research Foundation) grant 389792660 as part of TRR 248, see https://perspicuous-computing.science.


Jean-Bernard Stefani

Martin Vassor

Encapsulation and Sharing in Dynamic Software Architectures: The Hypercell Framework

We present in this paper a novel framework for the definition of formal software component models, called the Hypercell framework. Models in this framework (hypercell models) allow the definition of dynamic software architectures featuring shared components, and different forms of encapsulation policies. Encapsulation policies in an hypercell model are enforced by means of runtime checks that prevent a component, in a given context, to evolve in violation of these policies. We present the main elements of the framework, its operational semantics and the first elements of its behavioral theory. We give some results concerning its ability to express different forms of composition, and show by means of examples its ability to deal with sharing and different forms of encapsulation.

Introduction

Motivations. How do we formally model dynamic software architectures featuring both encapsulation and sharing? Can we define an operational semantics and behavioral theory for these architectures? These are the questions we deal with in this paper. By dynamic software architectures, we understand structured collections of software components and their inter-relations [START_REF] Bass | Software Architecture in Practice[END_REF], that can evolve over time, either spontaneously, for instance to adapt to changing operating conditions, or following external intervention, for instance for purposes of fault correction or functional update. By encapsulation, we understand forms of confinement and isolation between components, typically coupled with information hiding and abstraction, that ensure capabilities offered, and information maintained by a component, can only be accessed through designated interaction points or interfaces. Examples include the many forms of encapsulation that have been studied under the topic of aliasing control and ownership types in object-oriented programming [START_REF] Clarke | Ownership types: A survey[END_REF]. By architectures with sharing, we understand architectures where components can take part in different ensembles, compositions or aggregations, possibly with different attendant properties, e.g. in terms of encapsulation, lifetime and existential dependencies [START_REF] Barbier | Formalization of the whole-part relationship in the unified modeling language[END_REF]. Examples include architectures featuring common services, such as databases or logs, that can be used by software components at different levels in a software structure, and architectures featuring shared resources such as virtual machines or operating system processes. An example can illustrate the questions we are concerned with. Consider the architecture depicted in Figure 1. In the figure, a composite component C has two subcomponents, C 1 and C 2 , equipped with private log subcomponents L 1 and L 2 , that are provided as client-specific logs by a composite log service component L (in the picture, components are depicted as circles, and an arrow from component X to component Y can be read as X contains Y , or Y is a subcomponent of X). The log service L is shared among the two subcomponents C 1 and C 2 . One can argue that each private log component L i (i = 1, 2) is participating to three different ensembles, C i , C and L. C i , because L i is existentially dependent on C i , and is partially encapsulated in C i as only updates originating from C i are possible (it is a partial encapsulation because not all communication between a component L i and its environment is mediated or controlled by C i ). C because each C i is a subcomponent of C, and C is supposed to encapsulate its subcomponents. L, because L i is existentially dependent on L, has the same lifetime as L (if L is deleted so are L 1 and L 2 ), and relies on private functions (e.g. data storage) provided by L. These ensembles also correspond to encapsulation scopes, whose meaning is, roughly, that no communication outside the scope is possible without explicitly passing through the top component of each scope (C, L, C 1 or C 2 ), except for the communications between C i and L i .

Related work. Over the past three decades, an abundant literature has developed that aims at formally modeling distributed, component-based, dynamic and adaptive software architectures, systems and services. One can cite notably: process calculi for distributed systems, such as π-calculi with localities [START_REF] Castellani | Process algebras with localities[END_REF][START_REF] Hennessy | Safedpi: a language for controlling mobile code[END_REF][START_REF] Riely | A typed language for distributed mobile processes[END_REF], Ambient Calculi and their variants [START_REF] Bugliesi | Access control for mobile agents: the calculus of boxed ambients[END_REF][START_REF] Cardelli | Mobile Ambients[END_REF], and Milner's bigraphs [START_REF] Milner | The Space and Motion of Communicating Agents[END_REF][START_REF] Sevegnani | Bigraphs with sharing[END_REF]; process calculi and formal models for service-oriented computing and adaptive systems [START_REF] Bruni | Reconfigurable and software-defined networks of connectors and components[END_REF][START_REF] De Nicola | A formal approach to autonomic systems programming: The SCEL language[END_REF][START_REF] Ferrari | Synchronised hyperedge replacement as a model for service oriented computing[END_REF][START_REF] Fiadeiro | A model for dynamic reconfiguration in serviceoriented architectures[END_REF][START_REF] Tutu | Service-oriented logic programming[END_REF]; formal software component models such as BIP [START_REF] Bliudze | A notion of glue expressiveness for component-based systems[END_REF], Ptolemy [START_REF] Eker | Taming heterogeneity -the Ptolemy approach[END_REF], Reo [START_REF] Jongmans | Overview of thirty semantic formalisms for Reo[END_REF], CommUnity [START_REF] Wermelinger | A graph transformation approach to software architecture reconfiguration[END_REF], and several others [START_REF] Leavens | Foundations of Component-Based Systems[END_REF][START_REF] Liu | Mathematical Frameworks for Component Software -Models for Analysis and Synthesis[END_REF]; formal software architecture description languages [START_REF] Magee | Dynamic structure in software architectures[END_REF][START_REF] Sanchez | Bigraphical modelling of architectural patterns[END_REF]. However, to the best of our knowledge, none of these previous works provide satisfactory support to model architectures featuring a combination of dynamicity, sharing and encapsulation. Synchronized Hyperedge Replacement (SHR) systems and location graphs constitute a direct inspiration for the work in this paper, but they do not allow the definition of encapsulation scopes with sharing. Ownership types allow the enforcement of encapsulation scopes in object-oriented programs, typically at the expense of restrictions in inter-object communication, but do not allow overlapping encapsulation scopes. Bigraphs with sharing [START_REF] Sevegnani | Bigraphs with sharing[END_REF] support the definition of nodes with overlapping containment scopes, but, as far as we are aware, it is not possible to use bigraph nodes to enforce the encapsulation policies considered in this paper. The Fractal component model [START_REF] Bruneton | The Fractal Component Model and its Support in Java[END_REF] is one of the rare software component models that allows the description of component configurations with sharing, and that has been formally defined [START_REF] Merle | A formal specification of the Fractal component model in Alloy[END_REF]. The architecture in Figure 1 can readily be described in Fractal, with encapsulation scopes captured by Fractal composites. But we do not have a formal operational semantics for Fractal that would allow us to define the exact semantics of these scopes, nor do we have a proper behavioral theory for Fractal architectures. Interesting approaches to enforcing encapsulation policies are works that rely on dynamic access protection instead of aliasing control. These include notably the Siaam actor abstract machine [START_REF] Claudel | Simple isolation for an actor abstract machine[END_REF], which relies on runtime checks to enforce actor encapsulation in a Java virtual machine, and access contracts [START_REF] Voigt | Access contracts: a dynamic approach to object-oriented access protection[END_REF] which provide dynamic access protection to Java objects that can support a wide range of encapsulation policies, including encapsulation policies with sharing as in the small architecture depicted in Figure 1. However, Siaam and access contracts do not come with a formal behavioral theory, and the question of program equivalence in concurrent languages with Siaam-like or access contracts-like access protection mechanisms remains open.

Contributions.

In this paper, we combine ideas from SHR systems [START_REF] Ferrari | Synchronised hyperedge replacement as a model for service oriented computing[END_REF], from location graphs [START_REF] Stefani | Components as location graphs[END_REF], as well as Siaam [START_REF] Claudel | Simple isolation for an actor abstract machine[END_REF] and access contracts [START_REF] Voigt | Access contracts: a dynamic approach to object-oriented access protection[END_REF] dynamic approaches to encasulation enforcement, to define a formal operational framework, called the Hypercell framework. This framework allows the definition of different software component models (hypercell models), that support the modelling of dynamic component ensembles (hypercells) with sharing and encapsulation. The Hypercell framework can be seen as a conservative extension and generalization of the BIP and Fractal components models [START_REF] Bliudze | A notion of glue expressiveness for component-based systems[END_REF][START_REF] Bruneton | The Fractal Component Model and its Support in Java[END_REF]. A main contribution of the Hypercell framework is how it handles encapsulation policies: to allow for maximum flexibility, they are enforced by runtime checks (authorizations), that prevent transitions of component ensembles that would violate the chosen policies. Defining a proper notion of authorization is not trivial however. In order to obtain a proper component theory (e.g. in the sense of [START_REF] Bauer | Moving from specifications to contracts in component-based design[END_REF]), we need a notion of hypercell equivalence that is a congruence for hypercell composition, and it is not clear how such a result can be obtained in presence of authorizations. The idea is to have authorizations operate only at the level of individual components (cells): this allows us to define a notion of hypercell bisimilarity where we can decouple the contribution of authorizations from the classical bisimulation game, which in turn allows us to obtain the required congruence result. However, this local form of authorization raises another problem: encapsulation policies are not local in nature, so how can we enforce them via such local checks, notably in presence of evolving component ensembles? We show, by means of examples, how this can be done via a combination of local but context-dependent authorization predicates and dynamic component types (cell sorts).

Outline. The paper is organized as follows. Section 2 is a brief informal introduction to hypercells. Section 3 presents the hypercell framework, and preliminary elements of a behavioral theory for hypercell models. Section 4 shows, by means of examples, how to enforce different forms of encapsulation using sorts and authorizations. Section 5 concludes the paper.

Informal introduction

A hypercell is a finite set of cells. A cell has (we also say "offers") roles (a term we borrow from location graphs). A role is a point of attachment for cells, as well as a point of interaction between cells. A hypercell, much like a SHR system, constitutes a hypergraph, where the roles are vertices, and cells are the edges of the hypergraph. A role corresponds to a point of attachment and interaction between cells, and may be offered at most by two distinct cells. Hypercells are thus limited forms of hypergraphs, where hyperedges can connect any number of vertices, but a given vertex can only be connected by at most two edges. As in standard software component model ontology [START_REF] Crnkovic | A classification framework for software component models[END_REF], roles are classified as provided or required : a provided role in a cell signals some service offered by the cell, whereas a required role signals some expected service. When a role belongs to two cells in a given hypercell (in required position in one cell, and in provided position in the other cell), we say that the role is bound, and that it binds the two cells that offer it. Otherwise, we say that the role is unbound.

A cell is a locus of computation, as are localities in process calculi such as the Distributed π-calculus [START_REF] Riely | A typed language for distributed mobile processes[END_REF], and Klaim [START_REF] De Nicola | Klaim: a kernel language for agents interaction and mobility[END_REF]. One can understand a cell as a basic software component or as a connector, as in the component-and-connector view of software architecture [START_REF] Bass | Software Architecture in Practice[END_REF] and in software component models [START_REF] Crnkovic | A classification framework for software component models[END_REF]. A hypercell can be understood as a composite software component or component ensemble. In this sense, the hypercell concepts align well with the standard concepts of software component models [START_REF] Crnkovic | A classification framework for software component models[END_REF] and software architecture, as present e.g. in the ACME [START_REF] Garlan | Acme: Architectural Description of Component-Based Systems[END_REF] and Fractal [START_REF] Bruneton | The Fractal Component Model and its Support in Java[END_REF] component models (cells and hypercells correspond to ACME and Fractal components, roles to ACME ports and Fractal interfaces, bound roles to Fractal primitive bindings).

Figure 1 depicts a small hypercell with roles drawn as black dots (or arrows when bound) and cells as ellipses. Interactions in a hypercell take the form of simple point-to-point bidirectional interactions between pairs of cells bound by some role. In Figure 1, cells C 1 and L 1 can interact directly because they are bound, but C 2 cannot directly interact with C 1 , nor C with L. In the architecture depicted in Figure 1, the scopes discussed in the introduction are manifested by bound roles and the sorts adorning the different cells (hinted at by arrows).

The behavior of a hypercell is the result of the composition of the behavior of its cells. A cell evolves by transforming into some hypercell, in the process possibly interacting with, or removing, cells it is bound to. The evolution of a hypercell corresponds to the parallel firing of a number of such cell transitions. An interaction between two cells bound at a role r amounts to several binary rendez-vous on communication channels succeeding at role r. An interaction will typically result in the simultaneous exchange of values at each of the channels participating in the interaction.

For instance, a client-server interaction at role r between a client cell C and a server cell S, may, on the server side, take the form r : {op v, resp , resp w }, where r is the role which appears in provided position in the server (hence the overline r), op is the channel on which the value v is sent, along with the return channel resp, and w is the value which is (instantly) returned by the server, in response to the request op v, resp , on the requested return channel resp. On the client side, the interaction would take the conjugate form r : {op v, resp , resp w }. Notice that we use an early form for interactions: this allows us, in the operational semantics of hypercell models, to abstract from syntactic details such as a distinction between sent values and receiving parameters (the latter typically under the scope of some binding constructs). Our operational semantics thus has no mention of substitution of values to formal parameters, but we do distinguish with channels between originating side (e.g. op, on the client side) and receiving side (e.g. op, on the server side).

Interactions between cells can be higher-order. In particular cells can be exchanged as values on channels during interactions. This allows the removal or passivation of cells as in the Kell calculus [START_REF] Schmitt | The Kell Calculus: A Family of Higher-Order Distributed Process Calculi[END_REF], which in turns allows to model objective reconfigurations in software architectures, where certain components can exercize explicit control over other ones.

Interactions between bound cells in a hypercell can be guarded by priorities. Priorities are crucial for the expressive power of the framework and the definition of different forms of composition operators as cells or hypercells. A priority allows a cell to check for the presence or absence of a signal from another cell it is bound to, in the form of the ability or inability to communicate on a given channel. For instance the client side communication above could be guarded by the absence of communication on channel sig on role s, which we would write thus: {s : ¬sig} • r : {op v, resp , resp w } . In effect, the possible emission of signal sig on role s preempts (takes priority over) the emission of the request op on role r.

Individual cell transitions are also guarded by authorizations. An authorization is a runtime check that determines whether a cell transition is licit or not. Authorizations rely on the hypercell context of an individual cell to make this determination. For instance, a cell within an encapsulation scope can be prevented from making a transition that would allow it to bind to a cell outside this scope, whereas the same transition of the cell outside of such a scope can be allowed to proceed.

We define in this section our Hypercell framework. This framework can be instantiated to yield different hypercell models. Each hypercell model must define the following sets: a set P of processes; a set S of sorts; an infinite set R of roles; a set V of values; an infinite set A of names; an infinite set Ch of channels; a set T u of unconstrained transitions; and an authorization predicate Auth. We require R ⊂ A, Ch ⊂ A, and that the sets P, S, and A be mutually disjoint. Values can comprise processes, sorts, and names as well as elements of other datatypes (booleans, integers, etc). Values can be exchanged between cells on channels at bound roles. We require that the set Ch contain the special channel rmv, which is used in hypercell models with objective cell removal. We require the set of names A to be equipped with an involution, called the conjugate operation, which sends a name a to its conjugate a. By definition, we have a = a, and we write a to denote a or its conjugate a.

We require that each of the sets above be equipped with an operation for swapping names: for any element x of the above sets, (r s) • x yields an element of the same set where names r and s have been permuted, i.e. where r is replaced by s. (in the long version of this paper, we require the datatypes above to be nominal sets [START_REF] Pitts | Nominal Sets: Names and Symmetry in Computer Science[END_REF], but for lack of space we do not go into details here). We also require the existence of an operation supp that extracts from an element the set of names it contains, and we write a#X for a ∈ supp(X).

Formally, a cell in a hypercell model is a 4-tuple of the form [P : s p • r], where P is the process of the cell, s is the sort of the cell, p and r are the sets of provided and required roles of the cell, respectively. If C = [P : s p • r], we have C.process = P , C.sort = s, C.prov = p, and C.req = r. Any cell C must meet the following constraints: C.prov∩C.req = ∅. The set of cells in a hypercell model is noted C. The process of a cell embodies its behavior; the fact that a process can be a value means that cells can potentially update their behavior dynamically. The sort of a cell is a dynamic type associated with the cell; sorts are used to enforce runtime constraints on cells, as is shown in Section 4.

A hypercell G is just a set of cells that meets the following constraints: for

any partition G 1 , G 2 of G (G = G 1 ∪ G 2 and G 1 ∩ G 2 = ∅), one must have G 1 .prov ∩ G 2 .prov = ∅ and G 1 .req ∩ G 2 .req = ∅,
where the set G.prov of provided roles of hypercell G is defined as C∈G C.prov (and likewise for the set G.req of required roles of G). We note 0 the empty hypercell, and H the set of hypercells in a hypercell model. We define the set of roles, of bound roles and unbound roles of a hypercell G:

G.roles ∆ = G.prov ∪ G.req G.bound ∆ = G.prov ∩ G.req G.unbound ∆ = G.roles \ G.bound
When G and G are two disjoint hypercells, we write G G to denote G ∪ G when G∪G is indeed a hypercell (i.e. a set of cells meeting the above constraints).

Operational semantics of a hypercell model

The operational semantics of a hypercell model is defined as a set T of labelled (contextual) transitions. A transition is an element of T = E × H × Λ × H, where E is the set of environments, and Λ is the set of labels. A label Λ is a pair π • σ , where π is a finite set of priorities, and σ is a finite set of interactions. We note the empty set of priorities or interactions. and we set π • σ .prior = π, π • σ .sync = σ.

A transition t = Γ, G, Λ, G ∈ T is noted Γ G Λ -→ G , with Γ ∈ E the environment t.
An interaction corresponds to an exchange of a value V on a channel c at a role r. An interaction takes the form r : c V if the role r is provided, and r : c V if the role is required. An interaction r : c V corresponds to a receipt on channel c at role r of value V , whereas an interaction r : c V corresponds to the emission of value V on channel c at role r. An interaction r : c V succeeds when matched with its conjugate interaction r : c V . Notice that the value V in a successful interaction must be the same on both emitter and receiver sides. For this reason, our presentation of an hypercell model transition relation can be said to follow an early style [START_REF] Sangiorgi | The π-calculus: A Theory of Mobile Processes[END_REF]. This allows us in the presentation of the hypercell framework to abstract away from syntactic details of interactions in hypercell models. We set (r : c V ).prov = {r}, (r : c V ).req = ∅, and the dual for r : c V . We set ( r : c V ).roles = {r} and ( r : c V ).channels = {c}. The set of interactions in a hypercell model is noted I.

A priority takes the following form: r : ¬c, where r is a role and c is a channel. Intuitively, a contraint r : ¬c stipulates that the cell bound at role r is not ready to perform an interaction on channel c. The set of priorities is noted Π. Priorities are inherited from location graphs and provide hypercell models with significant expressive power (see Proposition 1 below). We set ( r : ¬c).roles = {r}.

An environment Γ is a pair ∆ • Σ comprising a set of known names (roles or channels) ∆ ⊆ A = R ∪ Ch, and a skeleton hypercell (or skeleton, for brevity) Σ. For Γ = ∆•Σ we define Γ.names = ∆ and Γ.graph = Σ. The set of known names in an environment corresponds intuitively to the set of already generated names during a hypercell execution. New names created in a transition are names that do not belong to this set. The skeleton in an environment gathers information about the hypercell that surrounds the initial hypercell in a transition. It is used in determining authorizations for individual cell transitions (see rule Trans below). A skeleton cell is a triplet [s p • r]. The set of skeleton cells in a hypercell model is noted C s . The set of skeleton hypercells in a hypercell model is noted H s . Essentially, a skeleton is a hypercell where one has erased all the

Trans Γ.names • 0 C Λ -→ G Σ(C) ∈ Γ.graph Auth(Γ, C, Λ, G) Γ C Λ -→ G (Comp) Γ G1 π 1 •σ 1 -----→ G 1 Γ G2 π 2 •σ 2 -----→ G 2 CondP (s, π, π1, π2, Γ, C1, C2) CondI (σ, σ1, σ2, G1 G2) Cond(Γ, G1 G2) Γ G1 G2 π•σ ---→ G 1 G 2 (Ctx) Γ G •σ ----→ G IndP (s, π, , Γ, C, E) IndI (σ, E) Cond(Γ, G E, G E) Γ G E π•σ ---→ G E Fig. 2.
Transition rules for a hypercell model processes. The skeleton Σ(G) of a hypercell G is defined inductively as follows:

Σ(0) = 0 Σ([P : s p • r]) = [s p • r] Σ(G 1 ∪ G 2 ) = Σ(G 1 ) ∪ Σ(G 2 )
We denote by 0 the empty skeleton, and by E the set of environments in a hypercell model. We define

∆ 1 • Σ 1 ⊆ ∆ 2 • Σ 2 ∆ = ∆ 1 ⊆ ∆ 2 ∧ Σ 1 ⊆ Σ 2 , and ∆ 1 • Σ 1 ∪ ∆ 2 • Σ 2 ∆ = ∆ 1 ∪ ∆ 2 • Σ 1 ∪ Σ 2 .
An hypercell model must define the set T u of unconstrained transitions of its individual cells, i.e. transitions that do not rely on any knowledge of the execution context of individual cells. This fits with the idea that software components can be reused in different contexts (in our case, hypercells), and that their behavior should be defined as independently as possible from their context of use. We write Using terminology from [START_REF] Van Glabbeek | The meaning of negative premises in transition system specifications II[END_REF], the operational semantics of a hypercell model is defined as the set of transitions T ⊆ T that is the least well-suported model of the rules in Figure 2.

Γ C Λ -→ G for Γ, C, Λ, G ∈ T u .
Rule Trans turns an unconstrained transition into a regular transition, provided that it be authorized in the current context.

The predicates Cond, Cond I , Ind I in the premises of rules Comp and Ctx are defined as follows:

Cond(Γ, G) ∆ = supp(G) • Σ(G) ⊆ Γ CondI (σ, σ1, σ2, G) ∆ = σ = seval(σ1 ∪ σ2) ∧ σ.roles ⊆ G.unbound IndI (σ, E) ∆ = σ.roles ∩ E.roles = ∅ seval(σ) = if σ = { r : c V , r : c V } ∪ σ then seval(σ ) else σ
If C is a hypercell with r ∈ C.roles, such that there is a single cell L ∈ C with r ∈ L.roles, then we note C s r the hypercell (s r) • C. For ρ = r : ¬a, we define ρ.r = r. We say that hypercell C, in environment Γ , satisfies the priority constraint ρ = r : ¬a, noted C |= Γ ρ, if the following conditions hold:

Σ(C) ⊆ Γ.graph ∧ r ∈ C.unbound ¬(∃D ∈ H, V ∈ V, Λ ∈ Λ, Γ C Λ -→ D ∧ r : a V ∈ Λ.sync)
The predicates Cond P and Ind P in the premises of the rules Comp and Ctx are defined as follows:

CondP (s, π, π1, π2, Γ, C1, C2)

∆ = s#Γ.names ∧ π = {ρ ∈ π1 ∪ π2 | ρ.r ∈ (C1 C2).unbound} ∧ ρ∈π 1 \π C1 s ρ.r C2 |=Γ ρ ∧ ρ∈π 2 \π C1 C2 s ρ.r |=Γ ρ IndP (s, π, , Γ, C, E) ∆ = s#Γ.names ∧ π = {ρ ∈ | ρ.r ∈ (C E).unbound} ∧ ρ∈ \π C s ρ.r E |=Γ ρ
The predicate Cond P expresses the fact that priorities that appear on roles that bind the hypercells C 1 and C 2 together must be verified. Priorities on roles that bind hypercells C 1 and C 2 are exactly those constraints ρ in the set (π 1 \ π) ∪ (π 2 \ π), where π is the set of priorities that appear on roles not bound in C 1 C 2 (since priorities that appear in a transition of a hypercell C are expected to adorn unbound roles in C). To check whether a priority ρ is satisfied, one considers a variant of configuration C 1 C 2 where the role ρ.r, in the hypercell from which the priority originates, is replaced by a fresh role. In effect, this replacement amounts to severing the binding ρ.r between C 1 and C 2 .

Remark 1. The definition of satisfaction for a priority by a hypercell is not entirely trivial because of cycles of constraints that may occur. As a sanity check, consider the two following examples, depicted in Figure 3. ------→ C, where L can interact with N on channel b, provided M is not able to interact on a. Verifying the satisfaction of the priority on role p consists in checking whether M L s p N , where s is fresh, can interact on channel a on role p, which amounts to check that M can interact on channel a on role p.

On the right, we are considering a hypercell A B, with the following transitions:

tA = Γ A q:¬b•{p:c,q:c} ----------→ A t A = Γ A •p:a ----→ A tB = Γ B p:¬a•{p:c,q:c} ----------→ B t B = Γ B •q:b ----→ B
In other terms, A can interact on channel c on roles p and q, provided B cannot interact on channel b on role q, and B can interact on channel c on roles p and q, provided A cannot interact on a on role p. To verify the satisfaction of the priority from A on role q, we have to check whether the graph A s q B, where s is fresh, can interact on channel b on role q, which amounts to check that B can interact on channel b on role q. This is the case because of transition t B . The priority from A on role q is thus not verified, and transition tA cannot fire in this configuration. Likewise, the priority from B on role p is not satisfied and transition tB cannot fire in this configuration.

In both examples, our rules give results that match the intuition: in the first case, we expect the priority on p to be satisfied merely if M cannot interact on channel a on role p, and in the second case we expect the hypercell A B to deadlock.

Rule Comp stipulates that a hypercell G 1 G 2 can evolve by combining a transition from G 1 and a transition from G 2 . The combination involves synchronizing interactions on roles that bind G 1 and G 2 (condition Cond I ) and verifying priorities on the roles that bind G 1 and G 2 (condition Cond P ). Rule Ctx stipulates that in a hypercell G E, hypercell G can evolve independently of E, provided G's interactions and priorities do not involve roles from E (conditions Ind I , Ind P ). Notice that both rules Comp and Ctx require the results of the transitions in their conclusion (G 1 G 2 and G E) to be hypercells. Note that both rules are stratified by the number of bound roles in a hypercell: the number of bound roles in

C 1 C 2 is one less than in C 1 s ρ.r C 2 .
Notice that, in contrast to other process calculi frameworks such as the ψcalculus [START_REF] Bengtson | Psi-calculi: a framework for mobile processes with nominal data and logic[END_REF] and SHR systems [START_REF] Ferrari | Synchronised hyperedge replacement as a model for service oriented computing[END_REF], hypercell models do not have a restriction operator à la π-calculus. In hypercells, events taking place at a role binding two cells are not visible outside of the two cells. This hiding provided by bound roles is actually enough to encode restriction as in the π-calculus. Our handling of name creation via environments is also unusual, again compared to the use of a restriction operator à la π-calculus. It is related to the nominal presentation of the π-calculus in [START_REF] Cattani | Models for name-passing processes: interleaving and causal[END_REF], but relies on name insensitivity instead of α-conversion. This is no way a limitation on the expressive power of the hypercell framework for the restriction operator, as well as any other composition operator definable by means of GSOS rules, i.e. structured operational semantics rules obeying the general format defined in [START_REF] Bloom | Bisimulation can't be traced[END_REF]. More generally we can prove that any GSOS language (as defined in [START_REF] Bloom | Bisimulation can't be traced[END_REF]) can be encoded as a hypercell model: Proposition 1. For any GSOS language L, there exists a hypercell model and an encoding • : L × R → P(H), such that for any P, Q ∈ L, a ∈ A, u ∈ R, we have P a -→ Q if and only if there exist ∆ ⊆ A, Λ ∈ Λ with u : a ∈ Λ.sync, C ∈ P u , and

D ∈ Q u , such that ∆ C Λ -→ D.
Similarly, we can prove that the π-calculus can be encoded as a hypercell model.

Behavioral equivalence for hypercell models

We define in this section a strong notion of behavioral equivalence for hypercell models, in the form of a bisimilarity relation.

G F , if supp(G) • Σ(G) supp(F ) • Σ(F ).

Definition 2 (Strong simulation).

A name insensitive binary relation on hypercells R ⊆ H×H is a strong simulation if, for all G, F ∈ R, G ∈ H, Λ ∈ Λ, the following properties hold:

1. G F and the unbound provided (resp. required) roles of G and F coincide.

For all

Γ ∈ E such that Γ ∪Σ(G) ∈ E, Γ ∪Σ(F ) ∈ E, if Γ ∪Σ(G) G Λ -→ G , then there exists F ∈ H such that Γ ∪ Σ(F ) D Λ -→ F with G , F ∈ R.
The main difference compared to the usual notion of strong simulation on labelled transition systems is the quantification on environments, which is necessary to take into account the effect of authorization functions. Note also that we require that a transition be simulated by a transition with the exact same label. This is a strong requirement but which can only be relaxed if one knows more about actions hypercells can take on values (e.g. if processes can only be exchanged and run -placed in a cell -, one may require only that they be similar, as in higher-order simulations).

Definition 3 (Strong bisimulation and bisimilarity).

A binary relation R ⊆ H 2 is a strong bisimulation if both it and its inverse relation R -1 are strong simulations.

Strong bisimilarity, noted ∼, is defined by ∼ ∆ = R∈S R, where S ⊆ P(H 2 ) is the set of all strong bisimulations.

Crucially, in any hypercell model strong bisimilarity is a congruence (meaning our notion of bisimilarity is a reasonable notion of behavioral equivalence for hypercells):

Theorem 1. In any hypercell model, for all G, F ∈ H, if G ∼ F , then for all E ∈ H such that G E ∈ H and F E ∈ H, we have G E ∼ F E.
The proof of this is left out for lack of space but it proceeds by showing, by induction on the maximum number of bound names in G E and F E, that the relation

R = {(G E, F E | G ∼ F )} is a strong bisimulation.

Encapsulation policies

We show in this section how to enforce different encapsulation policies in hypercell models. Specifically, we present a form of strict encapsulation, inspired by owner-as-dominator policies studied in ownership types [START_REF] Clarke | Ownership types: A survey[END_REF], and a weaker variant that allows software architectures with overlapping encapsulation scopes as in Figure 1. The challenge is of course to enforce these policies in the highly dynamic and concurrent setting of hypercell evolutions. Some notations first. For L, M ∈ C ∪ C s , we write L M to mean L and M are bound, i.e. (L.prov ∩ M.req) ∪ (L.req ∩ M.prov) = ∅. For F, G ∈ H ∪ H s , we write F G to mean F.roles ∩ G.roles = ∅.

Strict encapsulation

In this form of encapsulation, cells come in three disjoint categories: owner cells, owned cells, and free cells. Owner cells can be understood as composite components. The cells they own -their owned cells -are their subcomponents. Free cells are neither owner nor owned. The encapsulation policy we consider here takes the form of a structural invariant which ensures an owned cell cannot directly interact with cells which do not belong to its owner's group -made by this owner cell and all its owned cells. For simplicity, we have only a single level of ownership (owner cells cannot be owned). It is relatively straightforward to extend this policy to allow multiple levels of ownerhsip.

To capture this, we consider a hypercell model (actually a class of models) with sorts that take the form of 4-tuples k, p, o, r , where k ∈ { , ⊥} is a flag and p, o, r ∈ P fin (R). We set: s.flag = k, s.fprov = p, s.owned = o, s.freq = r, and write C.fprov for C.sort.fprov, C.owned for C.sort.owned, C.freq for C.sort.freq, C.flag for C.sort.flag. Flags in sorts are used to avoid race conditions in the parallel evolution of owner and owned cells in a owner group, which would break the global structural invariant (for instance two owned cells being bound, while their owner is splitting itself in two).

A cell C in this model is assumed to maintain the following invariant:

C.prov = C.fprov ∧ C.req = C.owned ∪ C.freq ∧ C.owned ∩ C.freq = ∅ (1)
We also require to identify in a transition label Λ the roles that are sent by the initial cell in the transition. We note Λ.sent the set of sent roles in Λ.

We define the following (these definitions apply to skeletons as well). The structural properties we expect are defined as follows. For any G ∈ H∪H s :

∀L, M ∈ G, L = M =⇒ scope G (L) scope G (M ) ∧ L.owned ∩ M.owned = ∅ (2) ∀L, M ∈ G, L M =⇒ M.owned = ∅ (3) ∀L, M, N ∈ G, L M ∧ M N =⇒ L M ∨ L = N (4)
Property [START_REF] Barbier | Formalization of the whole-part relationship in the unified modeling language[END_REF] states that the encapsulation scopes of two owners L and M in the same hypercell are necessarily distinct and they are bound by no role. Property (3) states that there is only a single level of ownership: an owner cannot be owned. Property [START_REF] Bauer | Moving from specifications to contracts in component-based design[END_REF] states that cells in the encapsulation scope of an owner can only be bound to cells in the same scope or to the owner itself. We write Inv(G) if properties (2), (3), and (4) hold for G (hypercell or skeleton).

We assume the existence of a predicate New ⊆ P(A) × P fin (A) × P fin (A) with the following properties (New can be defined constructively but we eschew this definition here for lack of space):

New(∆, A, B) =⇒ B ∩ (∆ ∪ A) = ∅ New(∆, A, B) ∧ New(∆, A , B ) ∧ A = A =⇒ B ∩ B = ∅
Incl(G, M ) ∆ = M.prov ∩ G.prov = ∅ ∨ M.req ∩ G.req = ∅
We now define the authorization predicate for our class of hypercell models with strict encapsulation. Predicate Auth is defined as follows. Auth(Γ, L, Λ, G) is true exactly in the cases below:

1. If ∃M ∈ Γ, M Σ(L)∧M.flag = , G.owned = ∅∧M Σ(G)∧Safe(Γ, M, G), and Λ.sent ⊆ supp(L). If the flag of its owner is up, an owned cell can reconfigure into an hypercell G provided all the cells in G remain owned by the same owner, and the roles of G are either existing roles of cells in the owner scope, or brand new ones. If a cell is owned, the only constraint on its transitions labels is that sent roles in a label be roles already known by L (i.e. new roles created during a transition cannot be immediately sent). 2. If L owner ∧ L.flag = ⊥, Inv(H(Γ, L, G)) ∧ Osafe(Γ, L, G) with:

H(Γ, L, G) ∆ = Σ(G) ∪ (scope Γ (L) \ {M ∈ scope Γ (L) | Incl(Σ(G), M )}) Osafe(Γ, L, G) ∆ = K∈G.owners Safe(Γ, L, scope H(Γ,L,G) (K))
and Λ.sent ⊆ supp(L) ∧ rmv ∈ Λ.sync.channels. If its flag is down, an owner L can reconfigure into an hypercell G, provided G and the cells in L's scope remaining after the transition (those such that incl(Σ(G), M ) have been removed) respect the global invariant Inv, and the roles in the scope of owners in G are either ones already in its scope, or brand new ones. If a cell is an owner, the same constraint as above on sent roles apply, but in addition it cannot be removed by any other cell. and Λ.sent ⊆ supp(L). A free cell can reconfigure into a hypercell G provided it respects the global invariant Inv, it does not insert new cells in the scope of existing owners, and the roles of cells in the scope of new owners in G are safe. Also, since it is not an owner, new roles created during a transition cannot be immediately sent.

Note that, with the above definition of Auth, in an environment Γ where cell L is owned and the flag of its owner M is down, i.e. ∃M ∈ Γ, M L∧M.flag = ⊥, then L cannot evolve in environment Γ .

The authorization predicate is quite permissive in the kinds of evolutions owner cells can perform. Notice in particular that owner cells may split or dissolve during execution, allowing e.g. for the transfer of owned cells from one owner to another. Likewise, owned cells can be freed by their owner and become owner cells later on. The dynamicity and concurrency in the class of hypercell models obeying strict encapsulation is much bigger than that allowed in the computational models underlying ownership types (either strictly sequential or actor like).

Predicate Inv is indeed an invariant for the class of hypercell models equipped with these sorts and authorization functions:

Proposition 2 (Inv is an invariant). For all Γ ∈ E, G, G ∈ H, Λ ∈ Λ, if Inv(Γ ), Inv(G) and Γ G Λ -→ G , then Inv(G ).

Selective encapsulation

We extend the strict encapsulation policy of the previous section with a notion of weak ownership. Briefly, owner scopes of strict encapsulation are now allowed to include weakly owned cells. A cell may belong to only one owner, as previously, but may also belong to several weak owners. A cell can be weakly owned only if it has identified specific provided roles for this purpose (wprov roles below).

We extend sorts to 6-tuples k, p, o, r, q, w with q, w ∈ P fin (R). We set s.wowned = w and s.wprov = q. We write C.wowned for C.sort.wowned, and C.wprov for C.sort.wprov. C.wowned are required roles for binding to a weakly owned cell. C.wprov are provided roles for binding to a weak owner.

We adapt the invariant (1) as follows:

∀L, M ∈ G, L = M =⇒ scope G (L) scope G (M ) ∧ L.owned ∩ M.owned = ∅ (6) ∀L, M ∈ G, L M =⇒ M.owned = ∅ (7) ∀L, M, N ∈ G, L M ∧ M N =⇒ L N ∨ L = N ∨ M N ∨ N M (8)
Notice how the invariant (8) changes from the strict encapsulation policy. Cells in an owner scope are now allowed to bind to cells they weakly own, i.e. the weak ownership relation allows cells to bind roles across group boundaries. The authorization predicate for this new policy is defined as in the previous section, with just a change in the definition of the Safe predicate. Safe is now defined as follows: As it is, the selective encapsulation policy just allows for specifically identified roles to break the encapsulation policy, and for weakly owned cells to act as shared internal means of communication between different owner scopes. It is possible, however, to enforce additional constraints on weak ownership to reflect different aggregation semantics. For instance, one could enforce a lifetime dependency between weak owner and weak owned cell, preventing the removal of a weak owner if its weakly owned cells are still in place, or, one could ensure a cell has a single weak owner. We do not present these examples here, but our two examples in this section should provide a good taste of the possibilities offered.

Conclusion

We have presented the Hypercell framework for defining software component models (hypercell models). The basic ontology of any hypercell model agrees with the classical elements of software component models [START_REF] Garlan | Acme: Architectural Description of Component-Based Systems[END_REF][START_REF] Crnkovic | A classification framework for software component models[END_REF], but the combination of dynamicity, sharing and encapsulation an hypercell model can offer is, to the best of our knowledge, unique. The key points to retain are the following: (i) this combination is made possible by the use of contextual transitions, cell sorts and context dependent runtime checks that enforce encapsulation policies; (ii) a proper notion of equivalence between hypercells is obtained thanks to authorizations at the level of individual cells and a notion of bisimulation that decouples the effect of authorizations from the classical bisimulation game.

Our runtime approach to enforcing encapsulation policies seems more permissive, and able to express more forms of policies and aggregations semantics than possible with ownership types, as our examples suggest. However, we have at this time no formal proof of this. Also, how our approach compares with those combining static ownership discipline with dynamic ownership tests, as in the Mezzo permission-based language [START_REF] Balabonski | The design and formalization of Mezzo, a permission-based programming language[END_REF], remains to be seen. It is worth pointing out that in defining encapsulation policies in the Hypercell framework, we do have a choice between imposing static constraints on unconstrained transitions, and imposing dynamic constraints via authorization predicates. In this paper, we have opted in our examples for an approach that made maximal use of authorization, but other options are available that combine both. For expressivity, however, we believe some amount of run-time checking is inescapable.

A crucial question is of course whether our abstract Hypercell framework can be efficiently implemented and supported. An implementation of an abstract machine for object-based hypercells is currently under way, but is clear that enforcing encapsulation constraints via runtime checks is a viable option, as demonstrated by the work on Siaam [START_REF] Claudel | Simple isolation for an actor abstract machine[END_REF]. This work showed, in the simpler context of the actor model, that the overhead of such checks can largely be mitigated by means of static analyses that can safely remove most unnecessary ones.

Fig. 1 .

 1 Fig. 1. Architecture with sharing: shared log service

  env of the transition, G ∈ H the initial hypercell t.init of the transition, Λ ∈ Λ the label t.label of the transition, and G ∈ H the final hypercell t.final of the transition. Intuitively, if Γ G Λ -→ G , then hypercell G, when placed in environment Γ , can evolve into hypercell G provided the synchronizations in label Λ are met. The environment in a transition represents both the set of known names prior to the transition, and the hypercell context in which the initial hypercell of the transition is placed.

  Environments in unconstrained transitions are of the form ∆ • 0. An unconstrained transition ∆ • 0 C Λ -→ G for an individual cell C must obey the following conditions: (i) names in the support of C must be known names, i.e. names in ∆: supp(C) ⊆ ∆; (ii) interactions and priorities in Λ = π • σ must be offered at roles from C: σ.prov ⊆ C.prov ∧ σ.req ⊆ C.req and π.roles ⊆ C.roles. In addition, we require T u to be insensitive to name changes, namely: ∀t ∈ T u , n, m ∈ A, (n m) • t ∈ T u . An hypercell model can define cells that allow their removal by other cells they are bound to. A cell C that allows its removal on some role r must provide an unconstrained transition of the form ∆ • 0 C •{ r:rmv C } ---------→ 0. A hypercell model must define an authorization predicate Auth. Predicate Auth ⊆ E × C × Λ × H determines whether an individual cell transition is possible in a given context (a surrounding hypercell). We require Auth to be name insensitive, namely: for all n, m ∈ A, and cell transition t ∈ E × C × Λ × H, we have Auth(t) ⇐⇒ Auth((n m) • t).

Fig. 3 .

 3 Fig. 3. Two hypercells with priorities

Definition 1 (

 1 Environment equivalence). Two environments Γ, Γ are said to be equivalent, noted Γ Γ , if for all Υ ∈ E such that Γ ∪ Υ ∈ E and Γ ∪ Υ ∈ E, for all C ∈ C, Λ ∈ Λ, G ∈ H, we have Auth(Γ ∪ Υ, C, Λ, G) = Auth(Γ ∪ Υ, C, Λ, G). Two hypercells G and F are said to be environmentally equivalent, also noted

  For L, M ∈ C, we write L M for L.owned ∩ M.prov = ∅ (intuitively, L owns M ), and M.upL for L.owned ∩ M.prov when L M . If G ∈ H, we write L G to mean that, for all M ∈ G, L M . For G ∈ H, L ∈ C, we define scope G (L) = {M ∈ G | LM } (the set of cells owned by L), and group G (L) = {L}∪scope G (L). We write scope Γ (L) for scope Γ.graph (L). We drop the subscript G to write scope(L) and group(L) when the hypercell or skeleton context G is clear. An owner is a cell L such that L.owned = ∅ and we write L owner. We define: G.owners∆ = {M ∈ G | M.owned = ∅}. An owned cell L in a hypercell G is a cell such that there exists M ∈ G with M L.A free cell in a hypercell G is a cell which is neither owner nor owned.

  We define the following predicates, which are used in the definition of the authorization predicate. Predicate Safe ⊆ E × C × H is such that Safe(Γ, M, G) holds if roles of G are new roles or are roles already used in the scope of M in the context Γ . It is defined as follows:Safe(Γ, M, G) ∆ = ∃B ∈ P fin (R), New(Γ.names, H.roles, B) ∧ G.roles ⊆ B ∪ scope Γ (M ).roles Predicate Incl ⊆ H s × C s is such that Incl(G, M ) holds if M sharesa role with a skeleton cell in G. It is defined as follows:

3 .

 3 If L owner ∧ L.flag = , L.owned ⊆ G.owned, G ∈ C, and Λ.sent ⊆ supp(L) ∧ rmv ∈ Λ.sync.channels. If its flag is up, an owner can only change into a single owner cell, not losing any owned role, possibly adding some (e.g. to allow the reconfiguration of cells it owns). 4. If L free, Inv(G) ∧ Fsafe(Γ, L, G) where: Fsafe(Γ, G) ∆ = G.roles ∩ Γ.owned = ∅ ∧ K∈G.owners Safe(Γ, L, scope G (K))

C 5 )

 5 .prov = C.fprov ∪ C.wprov ∧ C.fprov ∩ C.wprov = ∅ ∧ C.req = C.owned ∪ C.wowned ∪ C.freq ∧ C.owned, C.wowned, C.freq mutually disjoint (For L, M ∈ C (or C s ), we write L M for L.wowned ∩ M.wprov = ∅. Writing now G.(roleswroles) for G.roles \ (G.wowned ∪ G.wprov), and F G for F.(roleswroles) ∩ G.(roleswroles) = ∅ he global structural invariant is now the conjunction of the following properties:

=

  ∃B ∈ P fin (R), New(Γ.names, M.roles, B) ∧ G.(roleswroles) ⊆ B ∪ scope Γ (M ).(roleswroles) ∧ G.wowned ⊆ Γ.wprov Using this policy, we can describe the architecture described in Figure 1 as a hypercell with cells C, C 1 , C 2 , L, L 1 , L 2 , where C and L are owners of cells C 1 , C 2 and L 1 , L 2 , respectively, and where C 1 and C 2 are weak owners of L 1 and L 2 , respectively.