Formal Verification of Time-Triggered Ethernet Protocol
using PRISM Model Checker