Section 17.2. SPECIFICATION
17.2. SPECIFICATIONThere is an emerging body of research in the area of aspect-oriented specification. In this section, we present some of the key research in this area with our emphasis being placed on formal approaches. The reason for this is twofold:
There is also, however, an expanding body of research on less formal approaches, such as approaches centered on UML. The interested reader is referred to the literature for a treatment on this subject, such as [3, 22]. Some key works will also be considered in the following design section. Some of the most important research in this area has been carried out at the Ecole des Mines de Nantes. In early work, Fradet and Südholt define a generic framework for AOP based on program transformation [33] (a similar approach is also advocated by Lämmel [56]). In particular, aspects are considered to be "program transformations acting on the syntax tree of the component program." Aspect weaving is then defined generically as the repeated application of such program transformations until a fixpoint is reached (i.e., until the transformation of the program is equivalent to the program itself). In subsequent work, they offer a formal definition of crosscuts based on the concept of execution monitors [29]. Execution monitors are concerned with the observation of events emitted during program execution or, more generally, patterns of events. On discovering a particular pattern, a particular action is executed (an aspect). A formal definition is provided for this event-based model, and a domain-specific language is then derived based on this formalism. A Java prototype is also described that, interestingly, is systematically derived from the language definition (by a translation from Haskell to Java). More recent work by this group, presented in [28], has further extended this approach to allow for the analysis of interactions between aspects; we include it in this section for completeness, but this work will be revisited in Section 17.6. Frequently, work within the specification domain attempts to build on previous research to provide a theory of aspects. For example, Katz and Gil examine the relationship between aspects and superimposition [47]. Superimposition is a concept developed in the distributed systems community whereby programs are considered as interleavings of subtasks, such as representing the core algorithm and other non-functional properties such as liveness. A language called SuperJ has also been developed based on the theory of superimpositions [74]. This language is implemented as a pre-processor to AspectJ. Other approaches advocate the use of process algebraic techniques [2], multiset rewriting [59], the use of the Temporal Logic of Actions [45], and also the theory of monads [26]. Finally, in links with the UML work mentioned previously, Aldawud, Bader, and Elrad consider aspect weaving and statecharts [1]. In this work, they achieve what they call implicit weaving through the use of the event broadcasting mechanism in statecharts. Formal verification inevitably brings with it the problem of state-space explosion, which is often alleviated by the use of techniques based on abstractions or symmetries. Within the context of model checking aspect-oriented programs, tools such as Bandera [24] have been used that employ program slicing techniques to generate partial models (based on the property to be verified). Some recent research by Ubayashi and Tamai employs this technique [82]. However, this suffers from the drawback of model-checking the already woven code (rather than model-checking taking place prior to weaving). Ongoing work at Lancaster is developing this further by generating a model that retains the aspect-oriented structure of the program for subsequent model checking [10]. A selection of the various techniques outlined previously is analyzed in more depth in Table 17-2.
The key choice here, with respect to which formalism to use, is exactly what is to be formally specified and, hence, what can be verified. If a formal specification of an entire system is required, including the behavior of the base system and the aspects, then the process algebraic approach of [2] is appropriate. Although the referenced work does not currently include tool support for analyzing the specifications, such support is available for the underlying formal notation (CSP). If, instead, specifications of the crosscuts (and subsequent analysis of them) are required, then the approaches based on execution monitors are appropriate [28, 29] (with the latter also providing support for interaction analysis; see Section 17.6). Finally, the work contained in the last two rows of Table 17-2 [74, 82] is different in that support for verification is provided by model checking. This is a very powerful and mature verification technique but unfortunately is one that can suffer from the state-space explosion problem. In this respect, the work of [82] is interesting in the use of program slicing (via Bandera) to reduce the state-space. To summarize, a wide range of approaches has now been developed for the formal specification of aspects, many building on theories emerging from other areas of computing. Further experience is required before a clear consensus can emerge from this work. |
EAN: 2147483647
Pages: 307