In this work, we develop a formal model of the AFDX frame management to ascertain the reliability properties of the design. To capture the precise temporal semantics, we model the system as a network of timed automata and use UPPAAL to model-check for the desired properties expressed in CTL. Our analysis indicates that the design of the AFDX frame management is vulnerable to faults such as network babbling which can trigger unwarranted system resets. We show that these problems can be alleviated by modifying the original design to include a priority queue at the receiver for storing the frames. We also suggest communicating redundant copies of the reset message to achieve tolerance to network babbling.