Formal verification is likely an alternative to check safety property of the system model. However, to design an abstract model of huge railway network manually may cause errors because of its complexity.This thesis proposes an alternative to generate a formal railway network model from the module of Timed Coloured Petri Nets. Instead of constructing the formal model of a railway network model from scratch using CPN Tools, we provide a set of predefined modules of the high-level railway network components, including a train station module, a rail module, etc. A set of mapping rules is provided to generate the high-level railway network in terms of modules, into Timed Coloured Petri Nets automatically by the developed tool. The resulting formal model is verified using CPN Tools to ensure the correctness, safety, and liveness of the formal railway network model.