A modern network is a complex distributed system and provides many challenges. One challenge is route updates which happen often and need to be performed consistently. This is a complex issue where solutions are still being developed. However, there has not been much focus on the time used for deploying a new configuration. In order to automate provably correct and optimize network updates, we present Timed-arc colored Petri net (TACPN) with formal semantics, a model where it is possible to model asynchronous concurrent systems such as a network. We propose an algorithm to unfold TACPN into a Timed-arc Petri net, where the unfolded model can then be verified by known verification engines. To create the models visually we have created a full implementation of TACPN into the tool TAPAAL. We make an encoding of networks in TACPN, where the networks have to hold the security policy Waypoint Enforcement (WPE). We present results from experiments where we create real-world topologies into TACPN and optimize the worst case update time between two configurations, while WPE still holds.