A Timed Colored Petri-Net modeling for precision time protocol

Precision Time Protocol (PTP) is clock synchronization protocol that is used in computer networks. It is one of the most widely used clock synchronization protocol in the domains where the high degree of precision is required. Accuracy of the PTP goes in the sub-microsecond range. A lot of works have been done for verification and simulation of the protocol. There are still lacks of formal model representations of the PTP in temporal interactions aspects. This paper proposes to use Timed Colored Petri Nets (TCPN) to model PTP and formally represent with temporal dimension. We will verify the model by means of simulation techniques.