TIMED ANALYSIS OF EMBEDDED NETWORKS USING TIMED AUTOMATA

Increasing communication needs of embedded systems lead to the integration of switched Ethernet, in order to bypass the bandwidth limitation of classical fieldbuses. This paper propose the use of timed automata and model checking in order to analyze the timing behavior of a network architecture including specific fieldbuses (CAN, FIP, …) interconnected by switched Ethernet. The architecture is decomposed into basic components modeled by timed automata. The modeling of the overall architecture is obtained by assembling basic components. Model checking then exhibits for instance worst-case delays scenarios.