Symmetry Reduction of Time-Triggered Ethernet Protocol | Zendy

Marwan Ammar | Zendy; Samir Ouchani | Zendy; Otmane Aı̈t Mohamed | Zendy

AI Assistant Blog Pricing

Home ZAIA Blog

Open Access

Symmetry Reduction of Time-Triggered Ethernet Protocol

Author(s) -

Marwan Ammar,

Samir Ouchani,

Otmane Aı̈t Mohamed

Publication year - 2013

Publication title -

procedia computer science

Language(s) - English

Resource type - Journals

SCImago Journal Rank - 0.334

H-Index - 76

ISSN - 1877-0509

DOI - 10.1016/j.procs.2013.06.039

Subject(s) - computer science , protocol (science) , ethernet , formal methods , model checking , formal specification , communications protocol , reliability (semiconductor) , local area network , computer network , formal verification , distributed computing , algorithm , programming language , medicine , power (physics) , physics , alternative medicine , pathology , quantum mechanics

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

The content you want is available to Zendy users.

Already have an account? Click here to sign in.

Having issues? You can contact us here

Accelerating Research