The　precise　generation　of　train　control　curves　for　the　on-board　Automatic　Train　Protection　(ATP)　of　the　Chinese　Train　Control　System　Level　2　(CTCS-2)　relies　significantly　on　accurate　train　control　engineering　data,　which　serves　as　a　critical　element　in　ensuring　the　safe　operation　of　trains.　However,　the　traditional　verification　methods　of　train　control　engineering　data　depend　on　manual　validation,　which　lacks　timeliness　and　completeness　and　makes　it　easy　to　overlook　potential　errors.　On　the　other　hand,　traditional　verification　rules　are　derived　from　railway　technical　specifications　and　standards,　expressed　in　textual　language　that　is　often　ambiguous,　which　leads　to　insufficient　completeness　in　data　verification.　To　address　these　challenges,　this　paper　proposes　a　formal　verification　method　for　train　control　engineering　data　based　on　a　Reduced　Ordered　Binary　Decision　Diagram　(ROBDD).　First,　the　attribute　constraints　of　the　train　control　data　and　the　implicit　constraint　relations　between　different　data　objects　are　mined　using　existing　railway　technical　specifications　and　expert　knowledge　of　railway　signals.　These　constraints　are　then　converted　into　Boolean　function　models.　Second,　we　formulate　the　ROBDD　generation　algorithm　and　the　evaluation　decision　algorithm　of　the　Boolean　function　using　the　equivalent　canonical　data　structure　ROBDD　of　the　Boolean　function.　Finally,　based　on　the　train　control　engineering　data　from　actual　passenger-dedicated　lines,　the　automatic　verification　method　is　developed　by　constructing　four　types　of　＂mutation＂　data,　including　mutate,　swap,　add,　and　remove.　The　test　cases　indicate　that　our　proposed　formal　verification　method　is　feasible　and　capable　of　achieving　high　efficiency　and　completeness　in　the　verification　of　CTCS-2　level　train　control　engineering　data.