Graduate Research Forum Details
Leverage Commonality at Model Level: Model Checking Smart Home Applications
| Author: | Zebin Chen |
|---|---|
| Date: | February 13, 2007 |
| Time: | 16:00 |
| Location: | 220 Deschutes |
Abstract
Our group is building Smart Home applications for the Cognitively Impaired population. We have chosen to work with an existing framework, OSGi, which allows us to develop specific applications more quickly. We use a combination of traditional testing and formal verification to insure these applications will cause no harm to the cognitively impaired users of our systems.
A major obstacle of using model checking is to build a checkable formal model. To ease model construction, we have built a formal model parallel to an OSGi framework, so that one can build a formal model for an OSGi application by filling some slots and hooks. This approach allows us to significantly reduce the efforts in model construction. However, difficulty arises when one has to vary features of the modeling framework to check different aspects of OSGi applications, e.g. the specialization code may have to scatter in multiple places of various Java files. We hypothesize that we can use Aspect-Oriented Programming techniques to solve such crosscutting concerns. In this talk, I will explain the motivation, proposed approach, potential problems (e.g. extra native code introduced by AspectJ), and show some existing results.