Computing the exact worst-case End-to-end delays in a Spacewire network using Timed Automata

Spacewire is a real-time communication network for use onboard satellites. It has been designed to transmit both payload and control/command data. To guarantee that communications respect the real-time constraints, designers use tools to compute the worst-case end-to-end delays. Among these tools, recursive flow analysis and Network Calculus approaches have been studied. This paper proposes to use the model-checking approach based on timed automata to compute the exact worstcase end-to-end delays and two case studies are presented