动态Petri网理论及其在移动计算服务组合中的应用

With the continuous development of new computing and electronic communication technology, formal verification theory of mobile cloud systems based on service and cloud computing has become the hotspot and difficult issues. This project is aimed at large-scale mobile cloud system to solve two key scientific problems for flexible modeling and dynamic optimization of service composition. Based on the theory of dynamic Petri nets, the formal theory and analysis method of flexible modeling and dynamic optimization are studied. Taking the mobile cloud systems as the application background, this project uses dynamic Petri nets to describe characteristics of system services (such as virtual, dynamic, loose coupling and reusability) and real-time properties of service composition (such as reorganization, routing and task transition). The model mechanism and formal semantics of dynamic Petri nets are analyzed. Then the modeling and well-formed verification method of service composition are applied for large-scale mobile cloud systems. On this basis, the adaptive evolution of dynamic optimization and evaluation method on service composition in mobile cloud systems is further studied. Finally, the dynamic service composition model of mobile commerce system based on cloud environment is analyzed and verified.

随着新型计算和电子通讯技术的不断发展，以服务和云计算为应用的移动云系统的形式化验证理论成为当前研究热点和难点问题。本项目面向大规模移动云系统，以解决服务组合的柔性建模和动态优化两个关键科学问题为主要目标；以动态Petri网理论为基础，开展柔性建模和动态优化的形式化理论及方法研究；以移动云系统为应用背景，利用动态Petri网刻画系统服务的虚拟性、动态性、松耦合、可复用、高度可集成等系统特性，以及服务组合的重组、路由选择和任务跃迁等实时属性，分析其模型机理和形式化语义，提供基于动态Petri网的大规模移动云系统中服务组合的柔性建模和良构性验证方法；在此基础上，研究移动云系统中服务组合自适应演化的动态优化及评价方法，并开展基于云环境的移动商务系统的动态服务组合模型分析验证研究。

本项目在随机Petri网的理论基础上开展了动态Petri网理论的相关研究，提出了动态随机Petri网（DSSPN）的概念，完善了动态随机Petri网理论，研究了移动云系统中服务组合的柔性建模问题。为了评价移动云系统的性能及基于动态随机Petri网研究移动云的资源动态优化问题，建立了移动云中服务组合的形式化模型，构建了服务组合评价指标体系，引入混合时变的多链接忆阻器神经网络预测动态系统的服务质量，并进一步研究移动云计算下资源动态优化问题及服务组合的建模、分析与验证。具体结果如下：（1）研究了动态Petri网理论及完备性问题，给出了动态Petri网可达性、有界性、活性的定义，分析了动态Petri网的代数性质；（2）研究了大规模移动云系统中服务组合的柔性建模问题，设计了快速求解S/T—不变量的算法，讨论了动态Petri网在不同范式下的转换规则，建立了基于动态随机Petri网对多目标任务调度问题和服务组合问题的形式化建模、分析与验证；（3）研究了云环境下移动商务的动态服务组合模型的系统性能，构建了包含效率、稳定性和用户体验三个维度的移动云系统性能评价体系，通过实验验证了算法的有效性和鲁棒性。本项目的研究成果不仅丰富和发展了动态随机Petri网的理论基础，同时也为移动云系统的建模和分析提供了一定的理论支撑。