Abstract: Route module is one of the important parts in railway station computer interlocking software, it can be modeled by using UML. For disadvantages that UML is lack of precise semantics, lack of model analysis and validation methods, Petri net, which has strict theoretical analysis method, was used to formal verifying for the module, ensure the accuracy and security of the module.