کد مقاله | کد نشریه | سال انتشار | مقاله انگلیسی | نسخه تمام متن |
---|---|---|---|---|
485501 | 703330 | 2013 | 8 صفحه PDF | دانلود رایگان |

Time-Triggered Ethernet is a relatively new protocol for safety-critical Local Area Network environments, known for its reliability and efficiency in providing seamless fail-safe communication. This paper presents a formal verification of the TTEthernet protocol, based on an interpretation of the TTEthernet specification document, applied to two formal network scenarios that represent a real-time, safety-critical setting. The conceptual model of both scenarios are modeled using the probabilistic timed automata, then, encoded into PRISM code. Also, a set of precise functional requirements is derived from the TTEthernet specification document and expressed using PCTL. Using this approach, the TTEthernet protocol was verified as applied to real-life network environments and one faulty state was identified within one of the settings, thus revealing a possible weak point in TTEthernet protocol.
Journal: Procedia Computer Science - Volume 19, 2013, Pages 273-280