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 AOPtechniques, I pre-process a generic modeling framework with pointcuts, inter-type definitions and other AOP constructs. The pre-processing step adds the only needed details to the bare essentials. While these details may be scattered in different parts of the application, with 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: one concerns native code and the other concerns performance penalties. I have created an abstraction library to resolve the native code in the AspectJ runtime library as needed, and have 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 mechanisms that have been widely used and cited. To patch such bugs, I propose a general solution to avoid data races during aspect instantiation for a class of applications based on the current AspectJ compilers.

This thesis includes both my previously published and my co-authored materials.