Search

Events and aspects that respond to them can and should be defined, specified, and verified in a modular way, as an aid in understanding and guaranteeing the correctness of each on its own. However, finding the appropriate interfaces and abstractions and expressing them precisely is not an easy task. Moreover, formally verifying large models is often unfeasible for existing model-checking tools.We present an abstraction refinement scheme to verify aspects and to define and correct both aspect and event specifications. This allows considering smaller models and learning the needed event guarantees at each step. In addition, this technique can be used to find sound abstractions to check event reachability. Moreover, the technique is applied for detecting interference in systems where there are responses to complex events and aspects may be activated within the execution of other aspects.

In this work we consider specification and compositional verification for interference detection when several aspects are woven together under joint-weaving semantics without recursion. In this semantics, whenever a joinpoint of an aspect is reached, the corresponding advice is begun even if the joinpoint is inside the advice of other aspects. This captures most of the possible aspect interference cases in AspectJ. Moreover, the given technique is used to capture cooperation among aspects, which enhances modularity. The extended specification and proof obligations should provide insight to the possible interactions among aspects in a reusable library.

By distinguishing between events and aspects, it is possible to separate the problem of identifying when an aspect should be applied, from what it must do. Observers (aspects that do not affect the state of the base system) are already part of aspect-oriented programming and language support is emerging for events that gather information and announce occurrence. The goal of compositional verification of events and observers is to prove that they are correct so that their guarantees may be used by other events or aspects. Moreover, a compositional verification model allows applying formal verification techniques in smaller models, and also building a library of events, in which for any base system that satisfies certain assumptions, the event detection will satisfy its guarantees. In this work compositional verification of events and observers will be defined to aid in the design of a framework that allows users to verify events, providing as well flexibility in the input language of the specification

AspectJ pointcuts relate to a specific execution point in the program and thus AspectJ is not capable of naturally expressing high-level events that are the culmination of a series of more basic events. Yet, there is a real need for expressing such events when dealing with domains having terminology at a level of abstraction higher than the program's code, e.g., software process support, usability evaluation of user interfaces, or detecting illegal banking practices. Here, we present a framework called HighspectJ that provides a structured AspectJ-based solution for defining and utilizing high-level events. The framework treats an event as a first-class object, separates between the identification and the treatment of the event, and facilitates definition of events in layers, where higher level events are defined in terms of lower level ones. In addition, definition and reuse of high-level events using aspects is facilitated by an event repository which contains event building blocks. The framework is described process support is given.

An extended specification for aspects, and a new verification method based on model checking are used to establish the correctness of strongly-invasive aspects, independently of any particular base program to which they may be woven. Such aspects can change the underlying base program variables to new states, and after the aspect advice has completed, the base program code continues from states that were previously unreachable.

Often, insertion of several aspects into one system is desired and in that case the problem of interference among the different aspects might arise, even if each aspect individually woven is correct relative to its specification. In this type of interference, one aspect can prevent another from having the required effect on a woven system. Such interference is defined and specifications of aspects are described. An incremental proof strategy based on model checking pairs of aspects for a generic model expressing the specifications is defined. When an aspect is added to a library of noninterfering aspects, only its interaction with each of the aspects from the library needs to be checked. Such checks for each pair of aspects are proven sufficient to detect interference or establish interference freedom for any order of application of any collection of aspects in a library. Implemented examples of interfering aspects are analyzed and the results are described, showing the advantage of the incremental strategy over a direct proof in space needed for the model check. Early analysis and detection of such interference in libraries of aspects will enable informed choice of the aspects to be applied, and of the weaving order.

Usually, aspects enhance a software product by being composed - or woven - into it. Here, on the other hand, we use aspects to support the software development process itself. The underlying system, i.e., the system to which the aspects are woven, is not the software product but the environment where it is developed. We define aspects to support both software process management and software process modeling. As we show, the aspects can monitor, enforce, or even partially implement compliance with desired development practices. They also provide a basis for a precise description of a software development process. As a case-study, we consider Extreme Programming (XP) and the Eclipse platform. XP is a software development methodology described by underlying values, principles and practices. We present examples of AspectJ aspects that support XP guidelines such as "compose tests before coding" or "provide rapid feedback". Their abstract definitions are shown to be platform independent and correspond to the XP ontology. Their concrete implementation and weaving is connected to Eclipse, an open-source development environment. The design and a prototype implementation of aspects for XP over Eclipse is described.

Support for the incremental design of aspects themselves has been neglected, even as the use of aspects in conjunction with underlying systems is gaining acceptance. The ways in which aspects can cooperate or interfere with each other need to be made explicit at the design level. An aspect architecture, a new software architecture viewtype, is proposed, and its general principles are explained. An instantiation for extending UML is described, where designs of aspects provide maximal flexibility, and a new concern diagram is provided to show how aspects can be combined to treat different concerns of a system. An example shows aspect architecture views of a digital sound recorder.

A superimposition is a program module that can augment an underlying distributed program with added functionality, while cutting across usual language modularity constructs like processes, packages, or objects. Two ways of combining superimpositions to create new superimpositions are presented. In sequential combinations a new superimposition is obtained that is equivalent to first applying one, and then applying the second to the result. In merging combinations, it is as if each component superimposition is applied independently to a basic program, without mutual influences.In both cases the applicability conditions and the result assertions of the component superimpositions are compared and used to determine whether the combination is possible. If so, they are then combined along with the code of the components to obtain both the specification and the code of the resultant superimposition, without considering any specific basic program. By using combinations of superimpositions from libraries, fewer components need be constructed manually, and programming techniques for independent issues can be codified. Among the examples we consider are versions of dining philosopher algorithms (exemplifying different scheduling techniques), a superimposition to make a program with a fixed number of processes able to handle process addition and deletion, and snapshot algorithms.

A self-stabilizing program eventually resumes normal behavior even if excution begins in, an abnormal initial state. In this paper, we explore the possibility of extending an arbitrary program into a self-stabilizing one. Our contributions are: (1) a formal definition of the concept of one program being aself-stabilizing extension of another; (2) a characterization of what properties may hold in such extensions; (3) a demonstration of the possibility of mechanically creating such extensions. The computtional model used is that of an asynchronous distributed message-passing system whose communication topology is an arbitrary graph. We contrast the difficulties of self-stabilization in thismodel with those of themore common shared-memory models.