可重写Petri网理论及在大规模动态分布式系统中的应用

With the rapid development of new-type computing technologies such as cloud computing, theoretical study of formal verification of large-scale dynamic distributed system being applied to sevice and cloud computing has been currently becoming a difficult and hot research topic. Taking the large-scale dynamic distributed system as the research object, this project focuses on two key problems of formal verification of flexible modeling and dynamic optimization of self-assembly. Particularly. Our research includes the following three aspects. Firstly, on the basis of rewriting theory of three rewritable Petri nets based on the position, transition and dynamic programming , we will research on the formal theory and method of flexible modeling and dynamic rewriting, and propose the properties preservation and inheritability detection algorihtms of the rewritable Petri nets. Secondly, with the application background of cloud computing system and sevices, we will analyse the modeling mechanisms and formal semantics of large-scale dynamic distributed system, and set up the methods of describing the system charactristics of virtualization, dynamic adaptivity, loose coupling, reusable and high integration baed on rewritable Petri nets, and propose large-scale dynamic distributed system construction and verification methods of formal semantics based on rewritable Petri nets thoery. Thirdly, we will research on dynamic evaluation and optimization methods of self-assembly evolution of cloud service system and dynamic service model analysis and verification of e-bussiness system such as staple commodity transaction based on the service architecture in the cloud envirimental.

随着云等新型计算的不断发展，以服务和云计算为应用的大规模动态分布式系统的形式化验证理论研究成为当前研究热点和难点问题。本项目面向大规模动态分布式系统，以解决柔性建模的形式化验证和自组装的动态优化两个关键科学问题为主要目标；以基于位置、变迁和动态编程三种可重写Petri网重写理论为基础，开展柔性建模和动态重写的形式化理论及方法研究，建立三种可重写Petri网的性质保持及继承性检测与分析算法；以服务和云系统为应用背景，利用三种可重写Petri网刻画系统的虚拟化、动态自适应、松耦合、可复用、高度可集成等系统特性，分析其模型机理和形式化语义，提供基于可重写Petri网的形式化语义的大规模动态分布式系统构造和验证方法；在此基础上，研究云服务系统自组装演化的动态评价及优化方法，并开展基于云环境下，基于服务架构的大宗商品交易系统等电子商务系统动态服务模型分析验证研究。

本项目自实施以来，课题组成员按照项目计划任务书的有关要求，在广泛查阅和检索国内外最新研究成果的基础上，开展了可重写Pe tri网理论、大规模动态分布式系统建模及分析等相关研究。重点建立了可重写Petri网的结构特点及分类体系和相应类型的可重写Petri网规则，分析了两类可重写Petri网保持 有界性（保守性）、可重复性（协调性）及活性等性质，给出了两类可重写Petri网保持 活性的充要条件，研究了位置和变迁可重写Petri网代数分析方法，分别建立了退化的位置（变迁）可重写Petri网模拟共享（同步）合成Petri网的算法，证明了共享（同步）合成Petri网是位置（变迁）可重写Petri网的一个实例。所得结果能够为大规模动态分布式系统的动态重构提供形式化建模方法，为大规模动态分布式系统的形式化验证提供有效途径。基于可重写Petri网的理论研究，深入开展了大规模分布式系统建模及性能评价研究，重点研究了大规模分布式系统虚拟化和可信认证等方面的建模分析及评价方法，计算中的资源动态优化配置等方面的内容，以及系统性能、资源及路由对大规模分布式系统可信性的影响。项目的研究为丰富和发展了Petri网的行为理论，为系统的行为表达、分析和性质验证 提供了新的理论基础。 . 项目实施以来，共发表论文15 篇，其中SCI检索12篇，EI检索11篇。培养硕士研究生18人，先后开展了同美国弗吉尼亚联邦大学、清华大学、北京大学、 同济大学等学术交流，邀请了北京大学何新贵院士、清华大学林闯教授、同济大学蒋昌俊教授、东南大学罗军舟教授等访问了课题组，并进行了学术交流。 申请举办2017年自动化学会网络信息服务专委会会议及第一届网路信息服务国际会议。 . 项目实施以来，经费支出在预算范围内得到有效合理使用。