The verification of a novel framework for real-time shared medium communication network protocols

The subject of this work is the real-time communication of the distributed industrial control applications over shared-medium Ethernet. We developed a framework for the real-time communication protocols over shared-medium Ethernet in our previous work. The framework is designed using the Timed Input/Output Automata formalism to serve the changing real-time communication needs of the embedded control applications. In this paper we present the modeling, simulation and formal verification process of the proposed framework using UPPAAL toolbox.