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

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

项目编号： No.61301158

项目类型： 青年科学基金项目

立项/批准年度： 2014

项目学科： 无线电电子学、电信技术

项目作者： 朱俊

作者单位： 中国人民解放军理工大学

项目金额： 23万元

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

中文关键词： 卫星通信；网络控制协议；无线资源管理；形式化建；运行时验证

英文摘要： 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

英文关键词： Satellite Communication；Network Control Protocol；Wireless Resource Management；Formal Modeling；Runtime Verification