【摘要】：自20世紀(jì)90年代W1eiser[’2]提出“普適計(jì)算”概念以來，嵌入式系統(tǒng)，無線通信等技術(shù)的發(fā)展為“服務(wù)無時(shí)不在，無處不在”的普適計(jì)算從理論變成現(xiàn)實(shí)提供了客觀的技術(shù)基礎(chǔ)。普適計(jì)算的目標(biāo)是將由網(wǎng)絡(luò)和傳感器以及移動(dòng)設(shè)備組成的信息空間和現(xiàn)在的物理空間結(jié)合起來，支持用戶隨時(shí)隨地獲取所需的服務(wù)。因此如何在普適環(huán)境下進(jìn)行有效的服務(wù)組合逐漸成為了一個(gè)熱點(diǎn)。 在普適環(huán)境下，不僅有網(wǎng)絡(luò)上的web服務(wù)，還有傳感器和移動(dòng)設(shè)備等提供的設(shè)備服務(wù)以及各類其他的服務(wù)，結(jié)合SOA思想[3]，共同組成了組合服務(wù)并將其最終構(gòu)建應(yīng)用模型。但是，由于普適計(jì)算環(huán)境所具有的自治性，動(dòng)態(tài)性和設(shè)備資源的約束性，使得在這樣的環(huán)境下進(jìn)行服務(wù)組合時(shí)面臨著特有的問題和挑戰(zhàn)[4]，比如服務(wù)組合過程中錯(cuò)誤的處理、檢測(cè)，，比如設(shè)備的動(dòng)態(tài)加入和刪除等。因此在普適環(huán)境中，如何為用戶提供可信的服務(wù)組合成為了普適環(huán)境下服務(wù)組合的關(guān)鍵問題。 本文分析了己有的服務(wù)組合的技術(shù)以及服務(wù)組合模型，并在此基礎(chǔ)上提出了一個(gè)基于抽象狀態(tài)機(jī)的服務(wù)組合模型，并提出驗(yàn)證方法。使用抽象狀態(tài)機(jī)對(duì)服務(wù)的行為進(jìn)行刻畫，能夠很好地對(duì)服務(wù)進(jìn)行不同精化層級(jí)上的形式化描述，從而達(dá)到不同層級(jí)的正確性驗(yàn)證需求。然后結(jié)合SPIN進(jìn)行安全性、可達(dá)性的模型檢測(cè)。最后本文在實(shí)驗(yàn)中利用工具CoreASM和SPIN對(duì)文中提出的服務(wù)組合模型進(jìn)行驗(yàn)證，從而保證服務(wù)組合的正確性。實(shí)驗(yàn)結(jié)果表明，我們所提出的服務(wù)組合模型和驗(yàn)證方法能夠較好地適應(yīng)普適環(huán)境下服務(wù)組合系統(tǒng)的需求，驗(yàn)證其正確性，對(duì)后續(xù)的基于這樣的服務(wù)組合的實(shí)際應(yīng)用和開發(fā)帶來積極的意義。
[Abstract]:Since the concept of "pervasive computing" was put forward by W1eiser in the 1990s, the development of embedded systems and wireless communication technologies has provided an objective technical foundation for "ubiquitous computing", which is characterized by "everywhere and everywhere" from theory to reality. The goal of pervasive computing is to combine the information space composed of network sensors and mobile devices with the present physical space to support users to access the required services anytime and anywhere. Therefore, how to perform effective service composition in a universal environment has become a hot topic. In the universal environment, there are not only the web services on the network, but also the device services provided by sensors and mobile devices, as well as all kinds of other services. Combined with the idea of SOA [3], the composite services are formed and the application model is constructed. However, due to the autonomy, dynamics and constraints of equipment resources in pervasive computing environments, there are unique problems and challenges to service composition in such environments [4], such as handling errors in the process of service composition. Detection, such as device dynamic join and delete, etc. Therefore, in pervasive environment, how to provide trusted service composition for users has become the key problem of service composition in pervasive environment. This paper analyzes the existing technology of service composition and service composition model, and then proposes a service composition model based on abstract state machine, and proposes a verification method. Abstract state machine is used to describe the behavior of the service, which can describe the service at different level of refinement well, so as to meet the requirements of correctness verification at different levels. Then the model detection of security and reachability is carried out in combination with spin. Finally, the service composition model proposed in this paper is verified by using CoreASM and spin in the experiment to ensure the correctness of the service composition. The experimental results show that the proposed service composition model and verification method can better meet the requirements of the service composition system under the universal environment and verify its correctness. It will bring positive meaning to the subsequent practical application and development based on such service composition.
【學(xué)位授予單位】：上海交通大學(xué)
【學(xué)位級(jí)別】：碩士
【學(xué)位授予年份】：2013
【分類號(hào)】：TP338;TP301.1

【參考文獻(xiàn)】

相關(guān)期刊論文 前5條

1 倪晚成;劉連臣;吳澄;;Web服務(wù)組合方法綜述[J];計(jì)算機(jī)工程;2008年04期

2 徐光yP ,史元春 ,謝偉凱;普適計(jì)算[J];計(jì)算機(jī)學(xué)報(bào);2003年09期

3 李力行;金芝;李戈;;基于時(shí)間自動(dòng)機(jī)的物聯(lián)網(wǎng)服務(wù)建模和驗(yàn)證[J];計(jì)算機(jī)學(xué)報(bào);2011年08期

4 馮名正;;Web服務(wù)組合研究綜述[J];計(jì)算機(jī)應(yīng)用與軟件;2007年02期

5 易良辰;黃林鵬;;基于抽象狀態(tài)機(jī)的普適服務(wù)組合分析與驗(yàn)證[J];微電子學(xué)與計(jì)算機(jī);2013年03期

相關(guān)碩士學(xué)位論文 前1條

1 歐國建;多嵌入式系統(tǒng)的多任務(wù)調(diào)度研究[D];重慶大學(xué);2007年

本文編號(hào)：2119581