[發(fā)明專利]對(duì)時(shí)間敏感網(wǎng)絡(luò)的調(diào)度及流量整形機(jī)制進(jìn)行形式化分析方法

有效

• 申請(qǐng)?zhí)枺?/td>: 202010080117.0
• 申請(qǐng)日: 2020-02-04
• 公開(kāi)（公告）號(hào): CN111614573B
• 公開(kāi)（公告）日: 2022-05-06
• 發(fā)明（設(shè)計(jì)）人: 趙涌鑫;呂錦;蒲戈光;劉虹
• 申請(qǐng)（專利權(quán)）人: 華東師范大學(xué);上海工業(yè)控制安全創(chuàng)新科技有限公司
• 主分類號(hào): H04L47/22
• 分類號(hào): H04L47/22;H04L41/14
• 代理公司: 上海德禾翰通律師事務(wù)所 31319
• 代理人: 陳艷娟

本發(fā)明公開(kāi)了一種對(duì)時(shí)間敏感網(wǎng)絡(luò)的調(diào)度及流量整形機(jī)制進(jìn)行形式化分析的方法，包括：確定TSN調(diào)度及流量整形機(jī)制的組成部分；根據(jù)確定的各組成部分，抽象出簡(jiǎn)單的調(diào)度及流量整形模型；根據(jù)抽象模型，確定模型的精化方案；對(duì)精化模型進(jìn)行形式化分析以及時(shí)間性能分析。本發(fā)明中，通過(guò)對(duì)TSN的調(diào)度和流量整形機(jī)制進(jìn)行形式化建模，不僅可以通過(guò)推理驗(yàn)證來(lái)保證最終的協(xié)議標(biāo)準(zhǔn)是否滿足時(shí)間敏感性的需求，確保協(xié)議標(biāo)準(zhǔn)的正確性和可靠性；而且，對(duì)抽象模型的改進(jìn)代價(jià)較低，對(duì)于協(xié)議標(biāo)準(zhǔn)的開(kāi)發(fā)和后續(xù)擴(kuò)展能夠提供一定的幫助，能夠節(jié)省開(kāi)發(fā)時(shí)間和成本；并且提供了可量化的指標(biāo)來(lái)比較不同調(diào)度機(jī)制的異同點(diǎn)及優(yōu)缺點(diǎn)。

技術(shù)領(lǐng)域

本發(fā)明涉及軟件技術(shù)領(lǐng)域，尤其涉及一種對(duì)時(shí)間敏感網(wǎng)絡(luò)(Time-sensitivenetworking，以下簡(jiǎn)稱TSN)的調(diào)度及流量整形機(jī)制進(jìn)行形式化分析方法。

背景技術(shù)

自從2012年，IEEE 802.1任務(wù)組成立TSN工作組至今，已經(jīng)開(kāi)發(fā)了許多標(biāo)準(zhǔn)，用于解決時(shí)間敏感網(wǎng)絡(luò)中數(shù)據(jù)的通信問(wèn)題，獲得工業(yè)界和汽車(chē)行業(yè)的廣泛關(guān)注。隨著TSN標(biāo)準(zhǔn)的不斷擴(kuò)大，TSN網(wǎng)絡(luò)環(huán)境自然也變得越來(lái)越復(fù)雜。因此，TSN網(wǎng)絡(luò)的安全性急需得到保證，以確保其能夠提供準(zhǔn)確、準(zhǔn)時(shí)、快速的數(shù)據(jù)通信，同時(shí)也能保證高可靠性和有界低時(shí)延。然而，目前的研究方法大多通過(guò)使用測(cè)試、仿真來(lái)對(duì)TSN的調(diào)度和流量整形機(jī)制進(jìn)行研究分析，推演出最壞情況下的端到端時(shí)延。這種方式通常具有不準(zhǔn)確性，并且是很容易出錯(cuò)的，并不能提供可信的計(jì)算結(jié)果。而形式化方法是基于嚴(yán)格數(shù)學(xué)基礎(chǔ)，對(duì)計(jì)算機(jī)硬件和軟件系統(tǒng)進(jìn)行描述、開(kāi)發(fā)和驗(yàn)證的技術(shù)。其數(shù)學(xué)基礎(chǔ)建立在形式語(yǔ)言、語(yǔ)義和推理證明三位一體的形式邏輯系統(tǒng)之上，在提高計(jì)算機(jī)系統(tǒng)的可靠性和安全性方面發(fā)揮了重要作用。因此，本發(fā)明提出一種對(duì)時(shí)間敏感網(wǎng)絡(luò)的調(diào)度及流量整形機(jī)制進(jìn)行形式化分析的方法，為T(mén)SN標(biāo)準(zhǔn)提供可信驗(yàn)證保障。

發(fā)明內(nèi)容

本發(fā)明的主要目的在于提出一種對(duì)時(shí)間敏感網(wǎng)絡(luò)的調(diào)度及流量整形機(jī)制進(jìn)行形式化分析的方法。

為實(shí)現(xiàn)上述目的，本發(fā)明提供一種對(duì)時(shí)間敏感網(wǎng)絡(luò)的調(diào)度及流量整形機(jī)制進(jìn)行形式化分析方法，其包括以下步驟：

步驟S11：確定TSN調(diào)度及流量整形機(jī)制的組成部分；

步驟S12：根據(jù)確定的各組成部分，抽象出簡(jiǎn)單的調(diào)度及流量整形模型；

步驟S13：根據(jù)抽象模型，確定模型的精化方案；

步驟S14：對(duì)精化模型進(jìn)行形式化分析以及時(shí)間性能分析。

所述步驟S11包括以下子步驟：

步驟S11-1：確定參與TSN調(diào)度及流量整形過(guò)程的組成部分；

步驟S11-2：確定TSN調(diào)度及流量整形機(jī)制各組成部分之間的關(guān)聯(lián)關(guān)系及交互關(guān)系。

所述步驟S12包括以下子步驟：

步驟S12-1：根據(jù)各個(gè)部分之間的關(guān)聯(lián)關(guān)系，將具有關(guān)聯(lián)關(guān)系的部分合并為一個(gè)子模塊，對(duì)子模塊進(jìn)行建模，用信道或者全局變量來(lái)建立各子模塊之間的交互關(guān)系；

步驟S12-2：根據(jù)確定的子模塊之間的交互關(guān)系，采用信道或者全局變量來(lái)建立模塊之間的交互。

本發(fā)明提供的對(duì)時(shí)間敏感網(wǎng)絡(luò)的調(diào)度及流量整形機(jī)制進(jìn)行形式化分析的方法，通過(guò)對(duì)TSN的調(diào)度和流量整形機(jī)制進(jìn)行抽象建模，首先能夠找到參與調(diào)度和流量整形的功能模塊，將復(fù)雜的調(diào)度及流量整形機(jī)制抽象為不同模塊之間的協(xié)同交互過(guò)程，使得調(diào)度過(guò)程清晰明了；其次，對(duì)模型進(jìn)行形式化分析可以保證TSN協(xié)議的安全性和可靠性，在此基礎(chǔ)上再進(jìn)行時(shí)間性能分析，可以提供極大的可信度。

另外，本發(fā)明提供的對(duì)時(shí)間敏感網(wǎng)絡(luò)的調(diào)度和流量整形機(jī)制進(jìn)行形式化分析的方法還可以具有如下附加技術(shù)特征：

優(yōu)選地，所述確定TSN調(diào)度及流量整形機(jī)制的組成部分，包括：