Formal modeling of concurrent AOP programs

In the last few years, a new trend in programming centered on a new paradigm called aspect-oriented programming(AOP) has emerged. AOP is based on the object-oriented programming and introduces a new concept, the aspect. The aspects model those features being in many objects of an application may change or evolve independently one from the others. Because of this independence, it is not easy to verify the correctness of the AOP programs. Moreover, the problem of verifying the correctness is harder and more important in the case of the concurrent AOP programs than ordinary ones. The paper claims that formal specification of concurrent AOP programs could be a powerful tool for their correctness verification. Such specifications have the. advantage that can be used to demonstrate important properties of AOP programs, like safety and liveness properties. The truth of some of these properties is formally proved on the AOP solution of the Producer-Consumer problem. Its specifications are constructed using the Temporal Logic of Actions. The program is written in AspectJ, the most popular language implementing the AOP paradigm.