Formal Modeling of Frame Selection in Asynchronous TSN Communications  

作　　者：Ershuai LI Xuan ZHOU Jinjing SUN Huagang XIONG Feng HE 

机构地区：[1]School of Electronic and Information Engineering,Beihang University,Beijing 100191,China

出　　处：《Chinese Journal of Electronics》2024年第2期549-563,共15页电子学报（英文版）

基　　金：supported by the National Natural Science Foundation of China(Grant No.62071023);the Technology Development Fund of Shenzhen(Grant No.2021SzVUP082).

摘　　要：The asynchronous time-sensitive networking(TSN)based on IEEE 802.1Qcr is expected to be a promising solution for the asynchronous transmissions of safety-critical flows without the support of clock synchronization.When the asynchronous traffic shaping(ATS)mechanism is adopted to meet the deadline requirements for transmissions of safety-critical flow,it is necessary to formally verify the real-time properties and corresponding network performance.However,it is still unclear how to build an efficient formal model to evaluate different frame selection methods during the ATS scheduling process,which originate from the dominations of priority or eligibility time.In this paper,we present a formal modeling framework to compare the impacts of different frame selection on transmission sequence under the ATS mechanism.According to the priority level(pATS)or eligibility time(eATS)for flows,two transmission selection methods in ATS are modeled and compared.Then,we verify the real-time properties of ATS.The result shows that the shaping-for-free property can be satisfied with the pATS method but can not be fulfilled with the eATS method.Besides,the timing analysis results illustrate that the eATS method can provide more fairness than the pATS method for the transmission of low-priority flows in TSN networks.

关 键 词：Asynchronous communications Time-sensitive networking Frame selection Asynchronous traffic shaping/IEEE802.1Qcr. 

分 类 号：TP393.11[自动化与计算机技术—计算机应用技术]