Computerized management of critical systems makes the issues of correctness and faultless flow of long-lived and continuously-running programs extremely important e.g., [6, 7]. Complex systems cannot be fully verified because their verification may require an unreasonable amount of time and space. The software industry tests software products extensively in order to eliminate bugs as much as possible. Normally, software is tested by executing a set of large, but length-bounded and non-exhaustive scenarios starting from a predefined initial state while each scenario is defined by a set of input/output sequences. Undesired and unplanned behavior (bug) may occur due to scenarios that were not tested prior to the software release. Software malfunctions may cause damage that can outweigh the software cost. Keeping all this in mind, a consumer of a critical system would like to have a warranty that such a system will operate properly.

The ideas of a classic distributed superimposition are used to design a new object-oriented version incorporating aspects. A superimposition is a collection of generic parameterized aspects and new classes (often singleton concrete classes). Superimpositions can be combined, either sequentially or in a merge, to create new ones. Superimpositions also include specifications about assumed properties of basic programs to which the superimposition can be applied and desired properties added by the superimposition. These specifications are used to define proof obligations for the correctness of superimpositions and to check feasibility of combining superimpositions. SuperJ, a notation and an implemented preprocessor over AspectJ, is described. SuperJ can be used to apply a superimposition to a basic system, generating concrete aspects from generic aspects and then weaving them to basic classes. Superimpositions are separately declared, specified and verified. Among the examples used to demonstrate the approach are a termination detection algorithm, a version of the Dining Philosophers Problem and a monitoring superimposition that gathers statistics on basic objects.