The Research About Dynamic Upgrading Of Pervasive Services In Formal Methods

As the technology of computer and internet is developing rapidly, pervasive computing, the newly emerging research field, is turning from a beautiful blueprint to a reality steadily. Pervasive computing is a kind of computing focused on users, which is the next generation of grid computing and distributed computing. In a pervasive environment, there exist all kinds of devices with capability of computing. They collect useful environment data through sensors, make inferences basing on these data and predefined policies and then provide a composed service to the user in a context-aware way. Thus pervasive computing is a highly human-oriented and intelligent computing type.In pervasive computing, if the function provided by each device is defined as a service, then a critical problem has to be solved which is about how to compose atomic services into a composed service in a correct way considering the user requirements. Unluckily, as devices in a pervasive environment are highly dynamic, we can not ensure the services provided by the them are always available. When a device leaves the current environment, we need to find a proper service to substitute the old one. Another case is when a service provided by a device is upgraded, we need a new service to substitute the old one. Furthermore, we want the upgrading process to be dynamic, which means the upgrading process does not interrupt the runtime of the old service.In order to meet these requirements, this article presents a new formal service and upgrading model basing on the research and comparison of existing service models and upgrading theories. This model introduces the concept of ontology in semantic web, describes the services and user requirements in the semantic level and defines the concept of a correct upgrading policy in three aspects: type safety, behavior consistency and the satisfaction of user requirements.Furthermore, we develop a dynamic upgrading platform of pervasive services according to the formal model. It is based on a highly dynamic SOA framework OSGi and the techniques of semantic web to make services composed automatically and upgraded dynamically according to user requirements. We also develop related GUI user interface to make the management of services by users convenient.