非确定型Web服务流程重组的可靠性验证技术

In cloud computing and big data environment, due to natures of variable granularity, data intensive, uncertainty and timeliness, the Non-Deterministic Web service consists of kinds of component services, among which they have numerous and complex relationships. It makes the change probably happened in their service processes. Thus, how to verify the reengineered service process is a key problem to guarantee the trustworthy of core logic business. In this project, the probabilistic model checking will be employed to study the service process modeling and quantitative verification of Non-Deterministic Web service-based process reengineering. The research contents include four parts: 1) the service model for describing new natures of Non-Deterministic Web service will be studied. 2) The service process reengineering method will be discussed. 3) The quantitative verification and optimization techniques for reengineered service process of Non-Deterministic Web service will be explored. 4) The prototype tool platform supporting Non-Deterministic Web service modeling and verification will be designed and developed. From the perspective of functional and non-functional formal verification of service process reengineering, this project aims to make sure that reengineered service process is reliable. The study will enrich the quantitative model checking technology to service computing and service network areas, which will help to improve the credibility of Web-based software in Internet. Therefore, it plays important theory guidance meanings in promoting the prosperity of modern service industry.

在云计算和大数据环境下，由于可变粒度、数据密集型、不确定性和时效性等新特征，非确定型Web服务成员众多，成员及成员间关系多变，使得服务流程可能随时发生变化，如何对重组后的服务流程进行可靠性验证是保障核心业务逻辑可信的关键问题。本课题拟采用概率模型检验技术研究非确定型Web服务流程重组的建模与定量验证，重点研究支持描述非确定型服务特征的服务模型，研究支持非确定型服务的服务流程重组方法，研究支持非确定型服务流程重组的定量验证与优化方法，研制支持非确定型服务可靠性的建模与定量验证的原型工具平台。本课题从服务流程重组角度对功能性和非功能性进行形式化验证，能确保非确定型服务流程重组是可靠的。因此，该项研究将丰富定量的模型检验技术在服务计算、服务网络等领域的应用和探索，有助于提高网络软件的可信性，对促进现代服务业发展具有重要的理论指导意义。

非确定型Web服务的表现形式、内部逻辑和交互过程更加复杂，使得Web服务的服务流程重组成为基于SOA的软件的一种新延伸，需要研究高效、可靠的服务流程重组技术。针对不确定性的环境采用概率模型检验技术研究非确定型Web服务流程重组的建模与定量验证，主要考虑失效概率等随机不确定性因素在服务流程上的影响。在模型建模方面，主要研究了状态图的形式化转化，基于序列图的形式化转化，BPEL模型形式化转化；同时开发了可视化服务流程验证平台，该平台集成了PRISM工具支持概率模型检验。在动态配置方法，研究了服务数据接口一致性问题，给出了基于工作流的服务流程动态配置，以及服务流程选取和基于模型的移动环境测试方法。在面向具体应用问题方面，研究了监控服务系统可靠性，给出了监控服务系统可靠性方法，探索了应用概率模型检验技术到基于服务接口的校园能耗设备监控方法和智能交通流和路径规划，以及商品评论推荐。此外，针对云渲染任务调度、异构Hadopp网络的服务加载平衡、阿里巴巴的余额宝数据分析等具体问题也研究了考虑概率因素来解决。在专利申请方面，申请了状态图转化验证方法，基于CPU与GPU混合的渲染方法，概率模型的云渲染平台任务调度系统及方法，面向云渲染的分布式文件系统及构建和访问方法，基于混合云的云计算应用架构及云计算服务方法，面向云渲染的异构集群管理系统及方法，基于本体库的标签管理方法。非确定型Web服务的服务流程重组可靠性验证技术的研究将对促进Web服务技术的发展、应用和推广具有重要的理论意义和应用价值，为工业界和学术界认知和利用非确定型服务提供参考。为服务经济的发展奠定技术基础，对于促进我国现代服务业的发展具有重要的理论指导意义，也能为我国现代服务业企业的发展提供有力的技术和方法支持。