Design-Level Detection of Interactions in Aspect-UML Models Using Alloy


sig Status {} 146 JOURNAL OF OBJECT TECHNOLOGY VOL 6, NO. 7 5 TRANSLATION OF ASPECT-UML MODELS INTO ALLOY one sig connected, disconnected extends Status{} Aspect-UML’s primitive types such as Booleans, Real, Date, etc. must be translated as if they were enumeration types. Function operating over these types must be explicitly translated into Alloy functions. Indeed, Alloy does not provide any other primitive data type than int. It does not even have a boolean type (see [11] for explanations). Alloy nevertheless offers a module containing a signature for boolean atoms, as well as a collection of functions simulating boolean operators. Translation of classes and aspects. From a data perspective, Aspect-UML classes can be seen as sets of objects sharing a common collection of attribute declarations. The same thing can be said about aspects with the little difference that they are singletons. A class C (resp. an aspect A) can reasonably be translated into an Alloy signature C (resp. A) containing a field fi with type C → Fi (resp. A → Fi) for each attribute fi : Fi, 1 ≤ i ≤ n declared in C (resp. A). Methods/advices are not translated into fields of a class/aspect signature. As briefly explained above, we rather reify them as atoms belonging to an abstract Operation signature. Yet, this is not altogether satisfactory. As we know, Alloy is a declarative language used to specify what a system do, rather than how it does it (like imperative languages would do). Intermediate states are not naturally taken into account by Alloy which only provides non mutable fields. We need to overcome this limitation to specify how advices are composed and what are their intermediate effects on object states. To achieve this, each field declaration (denoting a class attribute likely to evolve) is extended with a Time signature, as it is shown in the following example. open util/ordering[Time] as timeorder sig Time {} sig Connection { status: Status one -> Time, origin: Device, destination: Device-> Time} Attributes appearing in pre and post conditions of methods/advices are typically identified as the ones likely to evolve. These attributes, translated into signature fields, are ended by the Time signature. This is what we observe in the Alloy translation of the Connection class above. As specified by pre and post-conditions, connections can change status (e.g., change from disconnected to connected) as well as be transferred to a new destination. Both status and destination field types are therefore augmented with Time. Before the addition of Time, c.status denoted a single Status atom. It now becomes a relation while c.status.t denotes the status of connection c at time t. The Time dimension allows signature fields to keep VOL 6, NO. 7 JOURNAL OF OBJECT TECHNOLOGY 147 DESIGN-LEVEL DETECTION OF INTERACTIONS IN ASPECT-UML MODELS USING ALLOY trace of object attribute values at different times of an execution. Type Time is simply an ordered set of atoms. The ordering is managed by the parameterized module ordering provided by Alloy. Translation of Aspect-UML behavioral specifications The behavior of a particular Aspect-UML model is specified by annotations describing the respective pre and post conditions that methods/advices must satisfy. Some behavioral information is also given by the context passing constraints annotating pointcuts. Translation of advices and methods used as join points. Not all methods/advices declared in an Aspect-UML model need to be translated into Alloy. Methods which do not represent join points can be discarded, as well as advices which do not implement a pointcut. We also assume that method calls appearing in pre and post conditions are discarded and replaced by equivalent expressions containing attribute consultation and predefined functions only. Methods and advices related to a pointcut are the only operations which need to be translated into Alloy since they are the sole ones concerned by our aspect interaction analysis. According to our modeling strategy, each method and advice is translated into a signature extending an abstract signature called Operation defined as follows: abstract sig Operation { begin, end: Time}sig Operation { begin, end: Time} The Operation signature has two fields respectively used to record the beginning and ending time of an operation. The information is later used to sequentialize operations and to identify the effect of an operation on object states during some time interval. Given a method myOp(f1 : t1, ..., fn : tn), a concrete signature myOp is created which extends Operation. The myOp signature must also declare 1) a target field to record the object being invoked and 2) an additional field fi of type ti for each of its parameters. An atom from signature myOp represents a specific invocation of method myOp. Being reified into signatures (rather than translated into predicates), methods/advices can be managed uniformly within Alloy. They can be used in field, predicate and function declarations. Some operations can be defined as extensions of others and therefore reuse, for example, the arguments factored out by a parent operation. Since playing distinct roles in the weaving process, operations representing advices need to be distinguished from methods used as join points. This distinction is realized by the declaration of subtypes Advice and JP. 148 JOURNAL OF OBJECT TECHNOLOGY VOL 6, NO. 7 5 TRANSLATION OF ASPECT-UML MODELS INTO ALLOY abstract sig JP, Advice extends Operation{error: Boolean} fact indivisible {all op: JP+Advice | op.end =}sig JP, Advice extends Operation{error: Boolean} fact indivisible {all op: JP+Advice | op.end =} Although denoting disjoint sets, JP and Advice both gather operation instances involved in a weaving process which may or not result in a valid composition. To track potential composition errors, JP and Advice introduces a field error that is set to true when such an error is detected. The Alloy model must also assume AspectUML advices and join points to be atomic operations having a unitary duration. A fact named indivisible is added to specify these behavioral constraints. Facts applying to abstract signatures JP, Advices and Operation introduce the generic constraints that any join point or advice must respect. The specific behavior of an operation still needs to be specified. Aspect-UML suggests to do this by means of pre and post conditions. Aspect-UML pre and post conditions rely on a subset of OCL’s formulas which can be translated into Alloy constraints quite straightforwardly. Our translation is similar to the ones proposed in [14, 7, 6]. One must only be careful when translating access to an attribute. Accessing an attribute a of an object o at a time t requires consulting signature field o.a and navigating through this relation to find o.a.t i.e. the value of the attribute at time t. Taken from our case study, here is an example of a join point specification translated into Alloy. sig Complete extends JP {self: Connection } { (self.status.begin = disconnected) //precondition => (self.status.end = connected) && //postconditions (self.origin.d_status.end = busy) && (self.destination.end.d_status.end = busy) && (self.origin.current.end = self) && (self.destination.end.current.end = self) && (error = False) else (error = True) } //error The join point described by signature Complete implicitly satisfies the generic constraints imposed to all JP atoms, while together satisfying the specific pre and post conditions introduced in the Complete signature fact. This join point has a single parameter self representing the connection targeted by the method call. To achieve a complete operation (line 7), a connection must a priori be disconnected (line 1) otherwise an error is signaled (line 8). At the end of its execution, the complete operation must leave the connection in a connected state (line 2), have marked the destination or origin devices as busy (lines 3-4), have linked origin and destination devices to the actual connection denoted by self(lines 5-6). The time values respectively associated to the before and after states of the connection are compelled to matched the begin and end field values of the Complete operation. We do not claim nor expect translating the whole OCL into Alloy. VOL 6, NO. 7 JOURNAL OF OBJECT TECHNOLOGY 149 DESIGN-LEVEL DETECTION OF INTERACTIONS IN ASPECT-UML MODELS USING ALLOY Adding time to signature fields compels us to reason with dynamic domains. Not only do we need to specify what each operation changes in a system (using pre and post conditions), but we must also explicitly specify all the signature fields that it does not modify. This might be tedious if the number of unchanged fields is important for each operation. This matter is known as the frame problem. Fortunately, it can be solved without needing to explicitly state all the conditions that must not change with regard to each operation. A more succinct approach consists in adding explanation closure axioms [15] to assert which operations are likely to have modified some given field. In the case of Aspect-UML models, it comes to adding facts stating things such as ”if a field f has changed, then some advice or join point e happened”. Following this approach, a new fact called unchanged is added to our translation model, thus solving the frame problem succinctly and modularly. fact unchanged { all t: Time last | let t’= | some e: JP + Advice { ((current.t=current.t’) || (e in Complete && e.error = False)) && ((status.t=status.t’ && d_status.t=d_status.t’) || (e in Complete + OpCompleteInterrupting && e.error=False)) && ((interruptedC.t = interruptedC.t’) || (e in OpCompleteInterrupting && e.error = False)) && ((destination.t = destination.t’) || (e in OpCompleteForwarding && e.error = False))}} Translation of context passing constraints. In Aspect-UML, a pointcut is a sort of abstraction used to expose the context of a certain number of join points under a common interface. An aspect is said to implement a pointcut if it provides an advice of the right type to be executed either before or after one of the pointcut’s join points. An advice crosscutting a join point must be able to access the context in which the join point is executed. Pointcuts are used to pass the context of join points (i.e. its actual parameters) to advices in some generic way. In Aspect-UML models, each pointcut is annotated with a set of mapping rules specifying how to relate join points arguments to advice parameters. The Alloy translation of pointcuts therefore consists in creating a predicate passCtxt(p : JP ) enforcing the mapping of p’s actual parameters over the arguments of each crosscutting advice a. For example, in the Telecom application, a passCtxt(p:JP) predicate is created which, among others, forces context passing from join point Complete to crosscutting advices OpCompleteInterrupting and OpCompleteForwarding. pred passCtxt( p:PJ ) { (p in Complete => (Complete.self = OpCompleteInterrupting.c)&& (Complete.self = OpCompleteForwarding.c)) (p in Drop => ... ) ... } 150 JOURNAL OF OBJECT TECHNOLOGY VOL 6, NO. 7 5 TRANSLATION OF ASPECT-UML MODELS INTO ALLOY Translation of advice composition and weaving To model and analyze aspect interactions, the Alloy translation must show how aspects are composed together and how they are woven to the base model. As we did previously for join points and advices, we use abstract signature constrained by facts to specify composition and weaving operations. Alloy’s non-recursive functions and flat relations would not have been an appropriate choices to deal with the recursive composition of advices. This approach allows us to define a modular translation which avoid suffering from some of Alloy’s limitations. Composition of advices. According to the aspect paradigm, when a join point is reached during an execution, one or many advices may have been declared to execute at this point. Conflicts can arise if two or more advices require to execute exactly at the same time (i.e. either all before, or all after the join point). Aspect-UML allows developers to define a precedence relation between aspects. This relation can be used to solve out conflicts and therefore justify the sequential composition of two conflicting aspects. If no ordering is imposed, conflicting aspects can execute in any order. They are composed into a non deterministic sequence of advices. Each collection of before/after conflicting advices will therefore give rise to a composition of advices to be executed respectively before or after corresponding join points. The composition of advices is naturally defined as a recursive operation. Alloy does not allow recursion inside predicates and functions, but it does accept recursive relations. Taking advantage of this, we reify the composition operation into an Alloy abstract signature Composition extending the Operation signature previously defined. This Composition signature introduces two new recursive relations: comp1 maps the composition on either an advice or composition, while comp2 relates it to another composition. In short, a composition is either an advice or a pair of compositions. abstract sig Composition extends Operation{} {comp1: Composition + Advice, comp2: lone Composition}sig Composition extends Operation{} {comp1: Composition + Advice, comp2: lone Composition} As mentioned above, we need to distinguish sequential compositions from nondeterministic sequential ones. This is achieved by defining two sub-signatures SeqComposition, NDComposition extending Composition. The particular behavior of each kind of compositions is specified by a signature fact that constrains the beginning and ending time of the composition itself and of its nested components. Figure 2 schematizes the internal coordination constraints that each kind of compositions must satisfy. In Alloy, the two kinds of compositions are straightforwardly modeled by the signatures shown below. These signatures include facts entailing internal coordination constraints. Let’s remark the use of predicate lte (”less than or equal”) to ensure the end of an operation precedes the beginning of the next one. Forcing equality would have allowed no possibility for later interleaving. VOL 6, NO. 7 JOURNAL OF OBJECT TECHNOLOGY 151 DESIGN-LEVEL DETECTION OF INTERACTIONS IN ASPECT-UML MODELS USING ALLOY Figure 2: Coordination constraints for SeqComposition and NDComposition abstract sig SeqComposition extends Composition{} fact seqComposition {all s: SeqComposition | (s.begin= s.comp1.begin) && (no s.comp2 => s.end = s.comp1.end else (s.end = s.comp2.end && timeorder/lte(s.comp1.end, s.comp2.begin) ) }sig SeqComposition extends Composition{} fact seqComposition {all s: SeqComposition | (s.begin= s.comp1.begin) && (no s.comp2 => s.end = s.comp1.end else (s.end = s.comp2.end && timeorder/lte(s.comp1.end, s.comp2.begin) ) } abstract sig NDComposition extends Composition{} fact nonDeterministicComposition {all nd:NDComposition | no nd.comp2 => (nd.begin = nd.comp1.begin && nd.end= nd.comp1.end) else ((nd.begin = nd.comp1.begin && nd.end = nd.comp2.end && timeorder/lte(nd.comp1.end, nd.comp2.begin) ) || (nd.begin= nd.comp2.begin && nd.end = nd.comp1.end && timeorder/lte(nd.comp2.end = nd.comp1.begin)) ) }sig NDComposition extends Composition{} fact nonDeterministicComposition {all nd:NDComposition | no nd.comp2 => (nd.begin = nd.comp1.begin && nd.end= nd.comp1.end) else ((nd.begin = nd.comp1.begin && nd.end = nd.comp2.end && timeorder/lte(nd.comp1.end, nd.comp2.begin) ) || (nd.begin= nd.comp2.begin && nd.end = nd.comp1.end && timeorder/lte(nd.comp2.end = nd.comp1.begin)) ) } Given those signatures, conflicting sets of advices can now easily be translated into Alloy. Let Confl ≺ be a set of conflicting before advices partially ordered by a precedence relation ≺. Let a1 , a2 , ..., an be the list of ordered advices from Confl ≺ such that for each i = 1..n, a ≺ i is translated into an Alloy signature ad s i extending Advice. Similarly, let a 1 , a 6≺ 2 , ..., a 6≺ n be the list of unordered 6 advices from Confl ≺ such that for each j = 1..m, a 6≺ j is translated into an Alloy signature ad nd j extending Advice. The translation of the composition of advices in Confl ≺ consists of: 1. creating a collection of signatures seq1, ...seqn extending SeqComposition; i.e. ai ≺ ai+1 for each i = 1, ..n− 1, i.e. ∀j ∈ {1...m}.∀a ∈ Confl ≺ . ((a 6≺ j 6≺ a) and (a 6≺ a 6≺ j )) 152 JOURNAL OF OBJECT TECHNOLOGY VOL 6, NO. 7 5 TRANSLATION OF ASPECT-UML MODELS INTO ALLOY 2. creating a collection nd1, ...ndm extending NDComposition; 3. adding facts to constrain seqi, 1 ≤ i ≤ n and ndj, 1 ≤ j ≤ m signatures to behave as if composed in a structure having the following shape: nd1(ad nd 1 , nd2(ad nd 2 , ..., ndn(ad nd m , seq1(ad s 1, seq2(ad s 2, ..., seqn(ad s n, ∅)...)))...))) For this, each signature seqi, i = 1..n− 1 is added the constraint seqi.comp1 = adi && seqi.comp2 = seq(i+1). Since it ends the sequence, signature seqn is constrained by seqn.comp1 = ad s n && (no seqn.comp2). Similarly, each signature ndj, j = 1..m−1 is added the constraint ndj.comp1 = ad j && ndj.comp2 = nd(j+1). To link the non-deterministic composition of Confl ≺ to its sequential composition, we simply need to constrain signature ndm by ndm.comp1 = ad nd m && ndm.comp2 = seq1. Accordingly, nd1 denotes the composition of all advices in Confl bef ≺ . Facts constraining NDComposition and SeqComposition ensure nd1 to denote all the possible interleaving of advices in Confl ≺ with respect to precedence relation ≺. In the Telecom application the signature shown below describes the non deterministic composition of the two advices OpCompleteInterrupting and OpCompleteForwarding. (We eliminated the empty set at the end of the composition.) It is worth remarking that the sequential composition of these two advices would differ from the one given below (for the non-deterministic sequence) only by removing the name of the extended class NDComposition and changing it to SeqComposition. sig Compos extends NDComposition fact compos {all s:Compos| s.comp1= OpCompleteInterrupting && s.comp2=OpCompleteForwarding }


    4 Figures and Tables

    Download Full PDF Version (Non-Commercial Use)