论文标题
SRP和CSRP的Uppaal模型的描述以及其终止和一致性属性的验证
Description of the UPPAAL Models for SRP and CSRP and Verification of their Termination and Consistency Properties
论文作者
论文摘要
创建了IEEE音频视频桥接（AVB）任务组（TG），以便为以太网提供柔和的实时保证。后来，TG被重命名为时间敏感的网络（TSN）及其范围扩大，以支持艰苦的实时和关键应用。流预订协议（SRP）是TGS的关键工作，因为它允许在网络中保留资源，并保证所需的服务质量（QOS）。 AVB的SRP基于分布式体系结构，而TSN基于集中式体系结构。在TSN中支持并使用了SRP的分布式版本。然而，它并非旨在提供对关键应用很重要的属性。因此，我们提出了一个新版本的SRP，并具有增强服务，称为一致的流预订协议（CSRP）。在本文档中，我们描述了我们开发的SRP和CSRP Uppaal模型以及用于验证其终止和一致性属性的查询。
The IEEE Audio Video Bridging (AVB) Task Group (TG) was created to provide Ethernet with soft real-time guarantees. Later on, the TG was renamed to Time-Sensitive Networking (TSN) and its scope broadened to support hard real-time and critical applications. The Stream Reservation Protocol (SRP) is a key work of the TGs as it allows reserving resources in the network, guaranteeing the required quality of service (QoS). AVB's SRP is based on a distributed architecture, while TSN's is based on centralized ones. The distributed version of SRP is supported and used in TSN. Nevertheless, it was not designed to provide properties that are important for critical applications. Therefore, we propose a new version of SRP with enhanced services called Consistent Stream Reservation Protocol (CSRP). In this document we describe the SRP and CSRP UPPAAL models we developed and the queries we used to verify their termination and consistency properties.
