多层卫星通信系统自主协同网络控制协议建模及运行时动态验证方法研究

In order to satisfy the development of future satellite communication systems, such as satellite constellation, multi-layer satellite nodes, amalgamation of several satellite communication networks etc., this fund project puts forward a method, in which several satellite/ground nodes self-collaboratively participate in satellite communication system network control task. The method includes the architecture of satellite self-collaborative network control, satellite network controlling mode and their switch mechanism, and resource and time restricted communication connection/switch control mechanism, so that system resources can be efficiently used and satellite viability can be greatly strengthened. Furthermore, for the sake of guaranteeing that self-collaborative network control mechanism and protocol can reliably and safely execute, it is need to perform the research work about formal modeling and correctness verification of network protocol during mechanism design to get rid of bugs as early as possible. This fund project focuses on reliability-dependence critical properties of network control protocol, concentrates on interactional protocol signaling, protocol interaction patterns and protocol interaction roll play. It gives out a Petri net based self-collaborative network control protocol formal description and modeling method. On the basis of this formal model, a distributed network control protocol runtime dynamic verification mechanism is brought out, in which protocol signaling captured in real time will be utilized to make a decision of correctness determinant of protocol execution by temporal properties consistency checking algorithm, so as to improve the reliability of network control protocol and satellite communication system.

为满足未来卫星通信系统星座组网、多层次、多网融合等发展的要求，提出多个卫星/地面节点自主协同参与网络控制任务的方法，研究卫星自主协同网络控制体系架构、网络控制工作模式及切换机制、响应时间和资源受限的通信接续切换控制机制，以高效利用系统资源、增强系统生存力。同时，为保证自主协同网络控制机制和协议可靠地运行，需在机制设计中即对网控协议展开形式化建模和正确性验证工作，尽早消除协议中可能存在的缺陷。项目聚焦于协议可靠性攸关的关键性属性，通过以协议信令交互为中心、以协议模式为基本研究粒度、以协议交互主体为角色分工，研究基于Petri网的自主协同网控协议的形式化描述和建模方法，并在此基础上深入研究分布式的网控协议运行时动态验证方法，通过实时捕获细粒度的协议交互信令作为运行时检测的事实依据，并经由时序属性一致性检测算法进行正确性判定，从而有效提升网控协议和系统运行的可靠性。

卫星通信系统正朝着多星组网、多业务融合、多种体制并存等趋势快速发展，呈现出高度的复杂性、异构性和动态特性。未来将出现结构更为复杂、规模更为庞大、交互更为频繁的卫星通信系统网络控制体系。为满足卫星通信系统发展的要求，本项目研究卫星通信系统自主协同网络控制机制及关键技术，探索一种新型的卫星无线资源虚拟化层次框架。在此框架基础上，进一步深入研究卫星无线资源虚拟化管理机制以及通信量感知的无线资源动态调度方法，以高效利用系统资源、增强系统通信能力。同时，为保证自主协同网络控制机制和协议可靠地运行，需在机制设计中即对网控协议展开形式化建模和正确性验证工作，尽早消除协议中可能存在的缺陷。项目聚焦于协议可靠性攸关的关键性属性，通过以协议信令交互为中心、以协议模式为基本研究粒度、以协议交互主体为角色分工，研究基于Petri网的自主协同网控协议的形式化描述和建模方法，并在此基础上深入研究分布式的网控协议运行时动态验证方法，通过实时捕获细粒度的协议交互信令作为运行时检测的事实依据，并经由时序属性一致性检测算法进行正确性判定，从而有效提升卫星网络控制协议和系统运行的可靠性。.经过近几年来的深入研究，本项目已取得了一系列论文、专利等方面的研究成果。同时，部分相关研究成果在其他项目中获得初步应用，对设计和研制卫星通信系统网络控制机制和提高网控系统可靠性、性能等方面将起到了一定积极的帮助作用。