Improving formal timing analysis of switched ethernet by exploiting FIFO scheduling

Ethernet is an emerging technology in the automotive domain and is capable to overcome the bandwidth and scalability limits of traditional buses like CAN or FlexRay. Formal performance analysis methods are required to verify the timing, e.g. by providing upper bounds on end-to-end latencies, in safety-critical real-time systems, such as automotive control and advanced driver assistance systems. In many real-time capable Ethernet implementations such as IEEE 802.1Q or AVB, frames can be prioritized and frames of equal priority are scheduled in FIFO order at the switch ouput ports. In this paper, we show how to exploit Ethernet's FIFO scheduling in a compositional formal performance analysis to derive tighter timing guarantees. In an automotive Ethernet setup, our proposed analysis leads to a significant reduction in end-to-end latency guarantees.