【摘要】 为了多机协同通信的机载环境中能够在线快速、高成功率完成时间敏感网络的业务调度解算，设计了一种基于Z3求解器的时间敏感网络流量规划调度方法。该方法根据不同业务的流量特征进行分类聚合优化并建立规划调度的约束模型，随后利用Z3求解器得到一种能够满足业务需求的网络规划方案。通过多机协同的典型业务流的模拟，验证了该方法能够得到可行的规划调度结果，相比于传统规划调度方法，该方法实现了嵌入式平台的在线部署与实时快速解算，且具有更高的求解成功率。更多还原

【Abstract】 To achieve fast and high-success-rate online scheduling and resolution of TSN(time sensitive network) traffic in aviation environments for multi-aircraft cooperative communication, a traffic planning and scheduling method for time-sensitive network(TSN) based on Z3 theorem prover was proposed. The traffic characteristics of different services were classified, aggregated, and optimized, and a constraint model for planning and scheduling was established. The Z3 theorem prover was employed to derive a network planning solution that satisfies the traffic requirements. Simulation results of typical multi-aircraft cooperative communication scenarios demonstrate that the proposed method produces feasible scheduling results. Compared to traditional planning and scheduling methods, this method enables online deployment on embedded platforms, provides real-time and rapid solving, and achieves a higher success rate in solving.更多还原