技术摘要：
本发明公开了一种对时间敏感网络的调度及流量整形机制进行形式化分析的方法，包括：确定TSN调度及流量整形机制的组成部分；根据确定的各组成部分，抽象出简单的调度及流量整形模型；根据抽象模型，确定模型的精化方案；对精化模型进行形式化分析以及时间性能分析。本发  全部
背景技术：
自从2012年，IEEE  802.1任务组成立TSN工作组至今，已经开发了许多标准，用于 解决时间敏感网络中数据的通信问题，获得工业界和汽车行业的广泛关注。随着TSN标准的 不断扩大，TSN网络环境自然也变得越来越复杂。因此，TSN网络的安全性急需得到保证，以 确保其能够提供准确、准时、快速的数据通信，同时也能保证高可靠性和有界低时延。然而， 目前的研究方法大多通过使用测试、仿真来对TSN的调度和流量整形机制进行研究分析，推 演出最坏情况下的端到端时延。这种方式通常具有不准确性，并且是很容易出错的，并不能 提供可信的计算结果。而形式化方法是基于严格数学基础，对计算机硬件和软件系统进行 描述、开发和验证的技术。其数学基础建立在形式语言、语义和推理证明三位一体的形式逻 辑系统之上，在提高计算机系统的可靠性和安全性方面发挥了重要作用。因此，本发明提出 一种对时间敏感网络的调度及流量整形机制进行形式化分析的方法，为TSN标准提供可信 验证保障。
技术实现要素：
本发明的主要目的在于提出一种对时间敏感网络的调度及流量整形机制进行形 式化分析的方法。 为实现上述目的，本发明提供一种对时间敏感网络的调度及流量整形机制进行形 式化分析方法，其包括以下步骤： 步骤S11：确定TSN调度及流量整形机制的组成部分； 步骤S12：根据确定的各组成部分，抽象出简单的调度及流量整形模型； 步骤S13：根据抽象模型，确定模型的精化方案； 步骤S14：对精化模型进行形式化分析以及时间性能分析。 所述步骤S11包括以下子步骤： 步骤S11-1：确定参与TSN调度及流量整形过程的组成部分； 步骤S11-2：确定TSN调度及流量整形机制各组成部分之间的关联关系及交互关 系。 所述步骤S12包括以下子步骤： 步骤S12-1：根据各个部分之间的关联关系，将具有关联关系的部分合并为一个子 模块，对子模块进行建模，用信道或者全局变量来建立各子模块之间的交互关系； 步骤S12-2：根据确定的子模块之间的交互关系，采用信道或者全局变量来建立模 块之间的交互。 本发明提供的对时间敏感网络的调度及流量整形机制进行形式化分析的方法，通 4 CN 111614573 A 说　明　书 2/7 页 过对TSN的调度和流量整形机制进行抽象建模，首先能够找到参与调度和流量整形的功能 模块，将复杂的调度及流量整形机制抽象为不同模块之间的协同交互过程，使得调度过程 清晰明了；其次，对模型进行形式化分析可以保证TSN协议的安全性和可靠性，在此基础上 再进行时间性能分析，可以提供极大的可信度。 另外，本发明提供的对时间敏感网络的调度和流量整形机制进行形式化分析的方 法还可以具有如下附加技术特征： 优选地，所述确定TSN调度及流量整形机制的组成部分，包括： 确定存储数据帧的数据结构； 确定网络中的同步时钟以及时间表； 确定预定义的传输选择机制。 优选地，所述根据确定的各组成部分抽象出简单的调度及流量整形模型，包括： 根据所述的存储数据帧的数据结构，确定数据模型； 根据所述网络同步时钟以及时间表，确定时间表模型； 根据所述预定义的传输选择机制，确定传输选择模型； 优选地，所述根据抽象模型，确定模型的精化方案，还包括： 根据所述数据数据模型，将数据帧表示为一个三元组： F＝(class，transTime，timestamp) 其中，class表示数据帧的类型；transTime表示数据帧的传输时间，由数据帧的长 度和网络带宽计算得出；timestamp表示数据帧到达交换机的时间。 将数据帧的存储结构定义为一个循环队列结构，表示为一个四元组： Q＝(prior，front，rear，seq[n]) 其中，prior表示队列的优先级；front和rear分别为队列的头指针和尾指针，指向 队首和队尾；seq[n]为存放数据帧的数组。 根据所述时间表模型，构建出时间自动机模型。 根据所述传输选择模型，构建相应的时间自动机模型。 分别确定各自动机模型之间的通信信道，用于时间自动机之间的同步； 确定系统中的其他元素，并使用变量在模型中表示出来，与时间相关的元素，使用 时钟变量表示； 确定时钟变量以及参与系统并发的自动机模型，构建并发系统。 优选地，所述对精化模型进行形式化分析以及时间性能分析，包括： 根据参与并发的模型，验证无死锁性； 根据模型的并发过程，跟踪状态变迁过程中形成的迹(trace)； 使用形式化语言描述系统的安全性质，并通过CTL公式进行描述，验证安全性质是 否满足； 根据所述并发系统形成的迹，记录在迹的最后一个状态(即系统停止并发的时刻) 的变量的值，以及在状态迁移过程中每个状态下变量的值，然后进行时间性能分析。 优选地，所述根据所述使用形式化语言描述系统的安全性质，并使用CTL公式进行 描述，并验证安全性质是否满足，包括： 所述安全性质是根据系统的需求规约得出，用形式语义对安全性质进行描述； 5 CN 111614573 A 说　明　书 3/7 页 根据安全性质的形式描述，用CTL公式表示，并对系统模型进行验证。 优选地，所述根据所述并发系统形成的迹，记录迹的最后一个状态的变量的值，以 及在状态迁移过程中每个状态下变量的值，进行时间性能分析，包括： 记录所述表示全局时钟的时间变量的值，以及被调度的数据帧的数量和每个数据 帧的传输时间transTime。 根据被调度的数据帧的数量和每个数据帧的传输时间可以计算出被调度数据帧 的传输时间总和。 根据表述全局时钟的时间变量在迹的最后一个状态下的值，以及被调度数据帧的 传输时间总和，可以计算出这段时间的时间效率。 根据所得并发系统的迹，可以得到每个状态下队列的状态以及队列中元素的调度 过程。根据队列中首元素从等待到被调度的时间差，计算出首元素的转发时延。 优选地，所述对并发系统进行形式化分析和时间性能分析，还包括： 选择不同的传输选择机制，参与到系统并发过程中，并对比不同的传输选择机制 的时间性能，得出不同传输选择机制的时间性能分析结果，并指导实际网络需求的部署。 本发明中，通过对TSN的调度和流量整形机制进行形式化建模，不仅可以通过推理 验证来保证最终的协议标准是否满足时间敏感性的需求，确保协议标准的正确性和可靠 性；而且，对抽象模型的改进代价较低，对于协议标准的开发和后续扩展能够提供一定的帮 助，能够节省开发时间和成本；并且提供了可量化的指标来比较不同调度机制的异同点及 优缺点。 本发明的附加方面和优点能够在下面的描述中部分给出，部分将从下面的描述中 变得明显，或通过本发明的实践了解到。 附图说明 通过阅读下文优选实施方式的详细描述，各种其他的优点和益处对于本领域普通 技术人员将变得清楚明了。附图仅用于示出优选实施方式的目的，而并不认为是对本发明 的限制。而且在整个附图中，用相同的参考符号表示相同的部件。在附图中： 图1为本发明实施例提供的一种对时间敏感网络的调度及流量整形机制进行形式 化分析的方法的流程示意图； 图2为本发明实施例提供的TSN调度及流量整形机制的示意图； 图3为对附图2所示TSN调度及流量整形机制的抽象模型的示意图； 图4为对TSN时间周期的划分示意图； 图5为本发明实施例提供的对TSN调度表模型建模示意图； 图6为本发明实施例提供的对TSN严格优先级传输选择模型建模示意图；