Research On Framework For Verifying AOP Programs Based On Runtime Verification

Object-Oriented Programming(OOP) is a programming criteria for software modularization and code reuse.OOP is a very good solution to the data and object encapsulations.However,with the rapid development of the programming methodology,adding crosscutting concerns such as optimizations tends to cause tangling and scattering of optimizing code over a program.Consequently,it is difficult to understand the codes and maintain programs.Aspect-Oriented Programming(AOP) is proposed to alleviate this problem and provides an effective and feasible method.Moreover,AOP supports reuse and modularity of code,which eliminate code tangling and scattering.With AOE program descriptions are divided into objects and aspects.A compiler,called a weaver,weaves aspects and objects together into one program.However,it is not easy to verify the correctness of a woven program because crucial behaviors including performance and synchronization are strongly influenced by aspect descriptions.Bugs tend to be embedded in aspects that may have complex structures to describe crucial behaviors.In order to solve such problems,an automatic verification approach will be used to check whether a woven program contains unexpected behaviors.The current research of AOP has focused on the language itself,but there are quite a few techniques that provide specification checking and verification.To solve the problem listed above,this paper presents a framework based on the Runtime Verification technique to verify the AOP programs and enables the verification on cross-cutting concerns of AOP programs.In this framework,the specification of a program is described by Linear Temporal Logic formulae,and the runtime verification of temporal properties occurs while the implementation procedure of the program.We design the whole flowchart,structure and the core algorithms and a detailed case study will be also provided to introduce the related research topics.