Formal Analysis And Construction For Internetware-based Software System

With the extensive application of Internet, the development, deployment and maintenance of software becomes open dynamic and uncontrollable. To accommodate the new requirements, software systems need evolving and multi-adaptive, which is so-called Internetware with characteristics of automation, coordination and evolution. This paper makes research on the construction and life cycle of Internetware and also proposes one formal model based on abstract state machine to analyze construct and verify internetware system. In addition, some smart home system cases are described.Major work in this paper includes:(1) Building DASM (Distributed abstract state machine) to form Internetware system and maps between distributed abstract state machine and internetware. In this model, one component maps to one sub-ASM whose input/output are also sub-sub-ASM interworking with monitor function. Internetware component itself and its related components constitute the running environment. Normal function provides background information by becoming monitor function in its abstract state machine. This Internetware model based on ASM can be easily verified abstract properties of target system requirements and make requirement clear before construction.(2) TO make it as accurate as possible when building model from the high level to the executable target system, one accuracy mechanism is proposed on Internetware model based on ASM. By studying the generic accuracy mechanism of Internetware model, this paper also give accuracy model of cooperation model in smart home architecture and pervasive Internetware platform based on OSGi. These accuracy models keep the original characteristics of target system and make consistent between the high level abstract internetware model and final model.(3) To find and fix the errors at as early stage as possible, abstract executive mechanism is designed to verify different level abstraction in Internetware accuracy. By executing this model, problems will be found during early design. In another aspect, accuracy models, which keep the procedure accurate, also make final system correctation.(4) Beside the above models, this paper also applies Internetware to solve problems in pervasive computing. Smart home architecture based on OSGi and R-OSGi is designed, in which a) direct service request cooperative model, b) cooperative model based on the publish/subscribe pattern of remote events, c) passive cooperative model, three cooperation models are supported. Experimental results show it is significant to development of internet ware.