I. Introduction
Future in-vehicle backbone networks will be based on Ethernet, as legacy buses such as CAN or FlexRay cannot keep pace with the growing bandwidth demands of advanced driver assistance systems (ADAS) or infotainment systems. Ethernet enables a scalable high-speed communication infrastructure and allows to realize arbitrary network topologies. However, Ethernet has a complex timing behavior. Thus, if safety-critical real-time applications are added to Ethernet, a formal analysis is required to verify that their timing requirements are met.