Formal verification of Time-Triggered Ethernet protocol using PRISM model checker

The Time-Triggered Ethernet (TTE) protocol is becoming widely used in safety-critical environments where failures cannot be tolerated. In this paper, a PRISM model for a TT-Ethernet is proposed based on its specification. A set of TTE properties is proposed as well. Finally, using PRISM model checker, a formal model is proposed in the form of a finite state machine. Using this approach, we were able to identify one faulty state within the network that might cause massive damage to a real-life application, thus revealing a possible weak point in Time-Triggered Ethernet.