Formal Modeling of Frame Selection in Asynchronous TSN Communications

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

作者机构：School of Electronic and Information Engineering Beihang University 

出 版 物：《Chinese Journal of Electronics》 (电子学报(英文))

年 卷 期：2024年第33卷第2期

页      面：549-563页

核心收录：

学科分类：0808[工学-电气工程] 08[工学] 081201[工学-计算机系统结构] 0812[工学-计算机科学与技术（可授工学、理学学位）] 

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

主　　题：System recovery Real-time systems Delays Synchronization 

摘      要：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 *** 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 ***, 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(p ATS) or eligibility time(e ATS) 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 p ATS method but can not be fulfilled with the e ATS method. Besides, the timing analysis results illustrate that the e ATS method can provide more fairness than the p ATS method for the transmission of low-priority flows in TSN networks.