Yevgenia Alperina, M.Sc. Thesis Seminar
Wednesday, 9.9.2009, 12:00
This work uses static data and control flow code analysis
to aid in proving properties of systems with aspects.
Some new categories of aspect advices (code segments) and
introduced methods are defined, beyond the existing ones.
The categories are chosen 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 based on forward flow analysis for
the detection of the categories is built, and applied to
benchmark aspect systems.