Improving formal timing analysis of switched ethernet by exploiting traffic stream correlations

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.