Do No Harm: Model Checking eHome Applications

Our group is building eHome applications for the cognitively impaired population. We have chosen to work with an existing framework, OSGi, that allows us to more quickly develop specific applications. We use a combination of traditional testing and formal verification to insure that the OSGi-based applications we build will cause no harm to the cognitively impaired users of our systems. This paper will focus on our results to date of using model checking to verify OSGi applications. In this paper, we describe the construction of a formal model parallel to the OSGi framework, which can be reused for rapid development of formal models for OSGi applications. With this approach, we have found the existence of stale references in several real examples. Stale references are a known concurrency problem in OSGi applications but difficult to get rid of. We argue that domain-specific reuse at the model level is an effective way to bring model checking closer to typical developers and tackle the concurrency errors. We also proposed and verified potential solutions, which can be used as generic paradigms to tackle the stale references problem in OSGi applications.