Formal Analysis of TSN Scheduler for Real-Time Communications

Time sensitive networking (TSN) is an emerging technology for in-vehicle networks, which has strict timing constraints and dependability requirements. The performance and efficiency of TSN depend on a reliable scheduling mechanism for real-time communications. Traditionally, the TSN scheduler is analyzed using simulations and testing, which are error-prone and inaccurate. In this article, we employ a timed model checker UPPAAL to formally model and analyze the TSN scheduler with a consideration of its transmission latency and time utilization. We first use the build-in assertion in UPPAAL to verify the deadlock-free property, safety property, and starvation-free property of our model. Then, we calculate the time utilization and the transmission delay of audio video bridging data frame under two scheduling mechanisms according to the simulation process. Then, we compared the time performance of this two scheduling mechanisms and found that each of them has their own advantages and disadvantages. This article provides a formal analysis framework for investigating scheduling strategies in TSN, which facilitates the designers to have a better understanding and development of TSN schedulers in the future.