In the last few years, a new trend in programming centered on a new paradigmcalled aspect-oriented programming(AOP) has emerged. AOP is based on the object-orientedprogramming and introduces a new concept, the aspect. The aspects model those featuresbeing in many objects of an application may change or evolve independently one from theothers.

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 caseof the concurrent AOP programs than ordinary ones. The paper claims that formal specificationof concurrent AOP programs could be a powerful tool for their correctness verification.Such specifications have the advantage that can be used to demonstrate important propertiesof AOP programs, like safety and liveness properties.

The truth of some of these properties is formally proved on the AOP solution of theProducer-Consumer problem. Its specifications are constructed using the Temporal Logic ofActions. The program is written in AspectJ, the most popular language implementing theAOP paradigm.