面向移动环境的服务流程可靠性定量验证与分析技术

With the fast development of mobile Internet and wireless communication technologies, more and more mobile devices have been popularized in our daily life. As an important research direction of the future Internet, how to implement target mobile service processes and ensure the availability and reliability before they are deployed to working environment should be addressed. Considering the changes of user location, the high frequency and instability of network connection, the limitation of service resources, the mobile Internet will seriously be impacted by the quality of service processes. To this point, the functionality and non-functionality of service processes are formalized from the perspective of service process and service quality, based on which quantitative verification techniques are employed in order to make sure the service process for mobile application is trustworthy. This project includes three parts: 1) the time constraint ordained mobile service process verification method will be studied by using timed model checking technology to verify the timed property, which mainly considers the limitation of internal services composition; 2) the probability ordained mobile service process similarity calculation method will be studied by using probabilistic model checking technology to verify the probabilistic property, which mainly considers random phenomenon of failures when interactions between two service processes are performed; 3) based on facts of time and probability, the prototype tool platform supporting quantitative verification of mobile service process for reliability analysis will be designed and implemented. Our research will contribute to guarantee the reliability of cross-organizational service process in the open, dynamic and uncertain mobile environment.

随着移动互联网的发展和移动终端设备的普及，如何实现移动环境下的目标服务流程并确保其可用性和可靠性是未来互联网发展的重要方向。考虑到移动网络的用户位置的变动性、网络连接的高频率不稳定性、服务资源的受限性将直接影响到服务流程的质量，本项目将从服务流程和服务质量角度，对服务流程的功能性和非功能性进行形式化建模，采用定量验证技术对其进行形式化验证，确保服务流程的可信。针对移动环境下服务流程内部服务组合的时间约束，重点研究基于时间约束的服务流程建模验证方法；针对移动环境下服务流程之间的服务调用和失效概率，重点研究基于概率验证的服务流程相似度计算方法；综合时间和概率两个因素，设计支持移动环境的服务流程可靠性定量验证系统框架，给出相关原型平台和实现方案。本研究将有助于实现跨组织服务流程应用在开放、动态、不确定的移动环境下，能够保证并提高服务流程的服务质量。

随着移动互联网的发展和移动终端设备的普及，如何实现移动环境下的目标服务流程并确保其可用性和可靠性是未来互联网发展的重要方向。移动网络的用户位置的变动性、网络连接的高频率不稳定性、服务资源的受限性将直接影响到服务流程的质量。在时间约束和形式化验证方面，提出了一种将业务流程执行语言(BPEL)转换为可用于形式化验证的时间自动机的方法，目的是将物联网服务组合的时间隐私需求进行形式化建模，并集合UPPAAL工具支持形式化验证。在应用概率模型检验和概率分析方面，提出了基于概率模型检验的多模式交通系统路径规划方法，实现了执行概率模型检查器PRISM并根据返回的定量结果进行分析和确认最优路径；提出了一种基于曼哈顿移动模型的可靠VANET路由决策方案，通过检查车辆与RSU之间的连通性，执行概率模型检验工具PRISM对各传输距离进行路由决策分析。在形式化方法和机器学习初探方面，针对手动编写检验性质问题，提出了一种基于GAN的检验性质自动生成(GAPG)方法，旨在训练生成更多新检验性质；其次，将形式化方法应用到垃圾邮件识别场景，对三种串通行为进行形式化建模，分析了垃圾邮件制造者的特点。在移动网络和无线场景应用方面，重点研究服务可用性和可靠性：利用协同计算和信息融合方法，提出了一种用于预测共享单车服务需求的方法，提高单车可用性；针对边缘计算下用户隐私保护问题，提出了一种加权噪声注入方法来保护用户的位置信息，同时向用户提供兴趣点POI推荐服务等。在专利方面，提出了一种面向位置感知的移动服务流程动态建模技术，支持形式化方法对移动服务流程的动态建模和形式化验证，尤其是概率模型检验，提高移动服务的服务质量。本研究有助于实现跨组织服务流程应用在开放、动态、不确定的移动环境下，能够保证并提高服务组合的服务质量。