Improving formal timing analysis of switched ethernet by exploiting traffic stream correlations
Improving formal timing analysis of switched ethernet by exploiting traffic stream correlations
复制标题
通过利用流量流相关性改进交换以太网的形式时序分析
DOI：
--
复制
发表时间：
2014
期刊：
影响因子：
--
通讯作者：
Jan R. Seyler
中科院分区：
文献类型：
--
作者：
Daniel Thiele;Philip Axer;R. Ernst;Jan R. Seyler
以太网在许多分布式嵌入式应用领域中变得越来越流行。在安全关键的实时系统中，例如工业控制或驾驶员辅助系统，需要正式的性能分析方法来验证时序，例如通过提供端到端延迟的上限。然而，这些形式化方法通常依赖于过度近似来将计算复杂性保持在易于处理的水平。在分布式系统中，这些过度近似可能会累积，导致过于保守的时序保证。交换网络，例如以太网（尤其是大型拓扑），特别容易受到这种影响。在本文中，我们确定了以太网中流量流之间的时序相关性，并展示了如何通过形式分析来利用它们来获得时序保证，该保证的严格程度高达 80%。
Ethernet networks become increasingly popular in many distributed, embedded application domains. In safety-critical real-time systems, such as industrial control or driver assistance systems, formal performance analysis methods are required to verify the timing, e.g. by providing upper bounds on end-to-end latencies. These formal methods, however, often rely on overapproximations to keep the computational complexity at a tractable level. In distributed systems, these overapproximations can accumulate leading to overly conservative timing guarantees. Switched networks, such as Ethernet (especially with large topologies), are particularly prone to this effect. In this paper, we identify timing correlations between traffic streams in Ethernet networks and show how they can be exploited by a formal analysis to derive timing guarantees, which are up to 80% tighter.