普适环境下基于抽象状态机的服务组合的分析与验证

发布时间：2018-07-13 13:48

【摘要】：自20世纪90年代W1eiser[’2]提出“普适计算”概念以来，嵌入式系统，无线通信等技术的发展为“服务无时不在，无处不在”的普适计算从理论变成现实提供了客观的技术基础。普适计算的目标是将由网络和传感器以及移动设备组成的信息空间和现在的物理空间结合起来，支持用户随时随地获取所需的服务。因此如何在普适环境下进行有效的服务组合逐渐成为了一个热点。在普适环境下，不仅有网络上的web服务，还有传感器和移动设备等提供的设备服务以及各类其他的服务，结合SOA思想[3]，共同组成了组合服务并将其最终构建应用模型。但是，由于普适计算环境所具有的自治性，动态性和设备资源的约束性，使得在这样的环境下进行服务组合时面临着特有的问题和挑战[4]，比如服务组合过程中错误的处理、检测，，比如设备的动态加入和删除等。因此在普适环境中，如何为用户提供可信的服务组合成为了普适环境下服务组合的关键问题。本文分析了己有的服务组合的技术以及服务组合模型，并在此基础上提出了一个基于抽象状态机的服务组合模型，并提出验证方法。使用抽象状态机对服务的行为进行刻画，能够很好地对服务进行不同精化层级上的形式化描述，从而达到不同层级的正确性验证需求。然后结合SPIN进行安全性、可达性的模型检测。最后本文在实验中利用工具CoreASM和SPIN对文中提出的服务组合模型进行验证，从而保证服务组合的正确性。实验结果表明，我们所提出的服务组合模型和验证方法能够较好地适应普适环境下服务组合系统的需求，验证其正确性，对后续的基于这样的服务组合的实际应用和开发带来积极的意义。
[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.
【学位授予单位】：上海交通大学
【学位级别】：硕士
【学位授予年份】：2013
【分类号】：TP338;TP301.1

【参考文献】