Dissertation Defense Details
Framework-based Model Construction with AOP assistance
| Author: | Zebin Chen |
|---|---|
| Date: | April 25, 2008 |
| Time: | 10:00 |
| Location: | 220 Deschutes |
| Committee: | Stephen Fickas, Computer Science (Chair) Michal Young, Computer Science Yannis Smaragdakis, Computer Science John Orbell, Political Science |
Abstract
I am part of a group that is building software for smart homes using a Java framework called Open Service Gateway Initiative (OSGi). Our concern is with proving certain properties correct about the framework and any application built on top of it. I have found it useful to take a model-checking approach to the proof problem. In recognition of the commonality of OSGi applications, I believe it is possible to build a modeling framework parallel to the OSGi specification to ease the model construction for OSGi applications.
I have tested the ideas by (a) constructing a modeling framework, and (b) model-checking several benchmark OSGi applications pulled off the web using that framework. The good news is that I was able to discover property violations in these applications through model checking, with relatively small efforts to formalize the applications. The bad news is that when checking certain applications, it requires customizations scattered in various places of multiple Java files, even including the modeling framework itself.
To accommodate such crosscutting concerns, I propose to use Aspect-Oriented Programming (AOP) to add another unit to modularize the needed changes. With AOP techniques, I pre-process a generic modeling framework with pointcuts, inter-type definition and other AOP constructs. The pre-processing step adds the only needed details to the bare essential. While these details may be scattered in different parts of the applications, with the AOP techniques I am able to specify such variations in an explicit and modular way. Varying application details then becomes a simpler task to specify and select the related aspects.
Two problems arise due to the adoption of the AOP techniques, i.e. the native code and the performance penalty. I have created an abstraction library to resolve the native code in the AspectJ runtime library as needed, and come up with a test suite in JUnit for regression test. The performance penalty is due to the internal variables used by aspect transformation and subsequent interleaving in a multi-threaded system. I thus make a distinction between model checking AspectJ applications in general and using AOP techniques to vary an existing formal model. For the latter problem, I present several approaches to reduce the search space, and am able to reduce the state space of an AspectJ program to a comparable size of its counterpart in pure Java implementation.
I have thus used the above technologies for rapid construction of formal models for OSGi applications. I am able to uncover several bugs in some benchmark OSGi applications with comparable search space. On the other hand, the extra interleaving of AspectJ programs suggests a potential data race. I have uncovered bugs in general Aspect-Oriented programming paradigm that have been widely used and cited. To patch such bugs, I propose a general solution to avoid data race during aspect instantiation for a class of applications based on the current AspectJ compilers.