|M.Sc Student||Alperin Yevgenia|
|Subject||Property Analysis and Automatic Detection of Aspect|
|Department||Department of Computer Science||Supervisor||Professor Shmuel Katz|
|Full Thesis text|
Aspect-oriented programming is a paradigm that allows modularizing cross-cutting concerns that are otherwise scattered or tangled in the system's code. Unfortunately, the addition of aspects to a system may influence its original state or control flow. This means that even an already verified system requires an additional heavy-weight verification process when aspects are added to it.
This thesis uses static data and control flow code analysis to aid in proving properties of systems with aspects. We extend the current repository of categories for classifying advices (code segments) and introduced methods of aspects. The categories are defined considering their effectiveness, in that they both provide real aid in verification of properties, and are automatically detectable using data and control flow. The theoretical part of the thesis investigates which linear temporal logic properties of a system are maintained when an aspect from the newly defined category is added. In the practical part of the work, an automatic tool called AsCat (Aspect Categorizer) is introduced for the detection of the defined categories. The tool is based on the AspectBench compiler, and uses its components such as the forward flow analysis of the Soot backend. To validate the results of our analyses, AsCat is applied to a number of benchmark aspect systems.