Evaluation of Real-Time Capabilities of Ethernet-based Automation Systems using Formal Verification and Simulation

Two main time features are identified in distributed automation systems, the update rate of Input and Output values and the end-to-end delay between a process event and its consequence. For the first feature, only the upper bound is needed, while for the second one, this is the whole distribution of delay values that shall be evaluated. In this paper, two methods are proposed to assess them in Ethernet-based automation systems using client-server protocols. First, timed model checking enables to determine a strict upper bound of update rate of Input and Output values. Secondly, Colored Petri Net simulation is used to forecast the whole distribution of end-to-end delays.