1.一种面向分布式路由协议的控制平面验证方法，其特征在于，所述方法包括：获取待验证网络的网络拓扑、配置和规约；利用图构建器将所述网络拓扑、配置和规约转化为一系列预设数据查询语言格式的事实；所述事实为所述网络拓扑、配置和规约的抽象表示；构建基于神经算法推理的控制平面验证模型；所述控制平面验证模型包括事实库嵌入、编码器、处理器和解码器；将所述事实输入所述控制平面验证模型，以使所述控制平面验证模型中的事实库嵌入将所述事实整合为事实图，所述控制平面验证模型中的编码器将所述事实图编码为隐空间表示；所述控制平面验证模型中的处理器利用归纳表示学习机制完善所述隐空间表示；所述控制平面验证模型中的解码器基于完善后的隐空间表示输出预测规约的满足性的布尔值；基于所述预测规约的满足性的布尔值确定控制平面验证结果。
2.根据权利要求1所述的面向分布式路由协议的控制平面验证方法，其特征在于，利用图构建器将所述网络拓扑转化为一系列预设数据查询语言格式的事实，包括：将网络拓扑中的节点按照角色的不同，划分为路由器、外部BGP对等体、路由反射器和网络前缀，并依次用 、 、 和 表示。
3.根据权利要求1所述的面向分布式路由协议的控制平面验证方法，其特征在于，利用图构建器将所述配置转化为一系列预设数据查询语言格式的事实，包括：对于OSPF协议，源节点 和目的节点 之间的链路权重 用 表示；对于BGP协议，同一AS内路由器 和 之间的内部BGP会话用 表示；属于不同AS的路由器 和 之间的外部BGP会话用 表示；封装BGP路由的属性用 表示；其中， 代表源实体 ， 表示网络前缀，整数 、 、 、 和 表示BGP路由的各种属性，包括本地偏好、AS路径长度、原始类型、多出口鉴别器值和社区标签。
4.根据权利要求1所述的面向分布式路由协议的控制平面验证方法，其特征在于，利用图构建器将所述规约转化为一系列预设数据查询语言格式的事实，包括：路由器 通过其邻居路由器 将流量转发到目标网络 用 表示；当目的地是网络 时，流量必须通过路由器 流向路由器 用 表示；从路由器 到目的地 通过其邻居 的流量，以及从路由器 到目标网络 通过 的流量是隔离的，用 表示。
5.根据权利要求1所述的面向分布式路由协议的控制平面验证方法，其特征在于，所述控制平面验证模型的表示为：其中， 为事实库嵌入中的嵌入函数，所述嵌入函数用于利用事实图中的局部节点特征信息为未见节点生成节点嵌入；所述嵌入函数 依赖于一组配置参数，包括 用于表示事实库 中的每个事实类型， 用于表示布尔值， 用于表示事实类型 的每个整型参数，以及 用于表示未知的规约满足度， 表示隐空间的维度， 代表支持的整数值的数量； 和 为事实图中每个节点 的中间节点表示， 为编码器，是一个图神经网络，由一个2层的SageConv模块组成； 为处理器，被建模为一个迭代过程，由一个6层的SageConv模块组成； 为解码器，用于为规约 的未知布尔值产生输出分布 。
6.一种面向分布式路由协议的控制平面验证系统，其特征在于，包括：处理器和用于存储能够在处理器上运行的计算机程序的存储器；其中，所述处理器用于运行所述计算机程序时，执行如下步骤：获取待验证网络的网络拓扑、配置和规约；利用图构建器将所述网络拓扑、配置和规约转化为一系列预设数据查询语言格式的事实；所述事实为所述网络拓扑、配置和规约的抽象表示；构建基于神经算法推理的控制平面验证模型；所述控制平面验证模型包括事实库嵌入、编码器、处理器和解码器；将所述事实输入所述控制平面验证模型，以使所述控制平面验证模型中的事实库嵌入将所述事实整合为事实图，所述控制平面验证模型中的编码器将所述事实图编码为隐空间表示；所述控制平面验证模型中的处理器利用归纳表示学习机制完善所述隐空间表示；所述控制平面验证模型中的解码器基于完善后的隐空间表示输出预测规约的满足性的布尔值；基于所述预测规约的满足性的布尔值确定控制平面验证结果。
7.根据权利要求6所述的面向分布式路由协议的控制平面验证系统，其特征在于，利用图构建器将所述网络拓扑转化为一系列预设数据查询语言格式的事实，包括：将网络拓扑中的节点按照角色的不同，划分为路由器、外部BGP对等体、路由反射器和网络前缀，并依次用 、 、 和 表示。
8.根据权利要求6所述的面向分布式路由协议的控制平面验证系统，其特征在于，利用图构建器将所述配置转化为一系列预设数据查询语言格式的事实，包括：对于OSPF协议，源节点 和目的节点 之间的链路权重 用 表示；对于BGP协议，同一AS内路由器 和 之间的内部BGP会话用 表示；属于不同AS的路由器 和 之间的外部BGP会话用 表示；封装BGP路由的属性用 表示；其中， 代表源实体 ， 表示网络前缀，整数 、 、 、 和 表示BGP路由的各种属性，包括本地偏好、AS路径长度、原始类型、多出口鉴别器值和社区标签。
9.根据权利要求6所述的面向分布式路由协议的控制平面验证系统，其特征在于，利用图构建器将所述规约转化为一系列预设数据查询语言格式的事实，包括：路由器 通过其邻居路由器 将流量转发到目标网络 用 表示；当目的地是网络 时，流量必须通过路由器 流向路由器 用 表示；从路由器 到目的地 通过其邻居 的流量，以及从路由器 到目标网络 通过 的流量是隔离的，用 表示。
10.根据权利要求6所述的面向分布式路由协议的控制平面验证系统，其特征在于，所述控制平面验证模型的表示为：其中， 为事实库嵌入中的嵌入函数，所述嵌入函数用于利用事实图中的局部节点特征信息为未见节点生成节点嵌入；所述嵌入函数 依赖于一组配置参数，包括 用于表示事实库 中的每个事实类型， 用于表示布尔值， 用于表示事实类型 的每个整型参数，以及 用于表示未知的规约满足度， 表示隐空间的维度， 代表支持的整数值的数量； 和 为事实图中每个节点 的中间节点表示， 为编码器，是一个图神经网络，由一个2层的SageConv模块组成； 为处理器，被建模为一个迭代过程，由一个6层的SageConv模块组成； 为解码器，用于为规约 的未知布尔值产生输出分布 。
