—　The　system　requirement　specifications　(SRSs)　of　the　train　control　system　(TCS)　are　the　starting　point　and　foundation　of　system　design　and　development.　Defects　in　the　SRSs　will　bring　great　risk　to　the　success　of　railway　engineering　projects.　Therefore,　formal　modeling　and　verification　methods　are　introduced　to　ensure　the　correctness　of　TCS.　However,　there　is　a　huge　gap　between　the　formal　computer　executable　model　and　the　SRSs　of　TCS　described　in　natural　language.　To　solve　this　problem,　a　complete　conversion　process　of　‘TCS　requirement　specification　→　semi-formal　models　(UML/SysML)　→　formal　models　(safety　verification　model　and　reliability　evaluation　model)’　should　be　created　to　ensure　full　coverage　and　consistency　of　semi-formal　models　and　formal　models　to　the　SRSs　of　TCS.　With　the　continuous　development　of　wireless　communication,　artificial　intelligence,　and　control　technology,　the　future　advanced　TCS　is　developing　towards　a　more　intelligent　and　autonomous　direction.　Online　safety　monitoring　and　operational　state-based　maintenance　approaches　are　critical　technologies　for　developing　the　future　advanced　TCS.　However,　the　traditional　model-checking　approach　is　time-consuming　and　susceptible　to　state　space　explosion　problems.　To　reduce　the　difficulty　of　online　safety　monitoring　and　reliability　evaluation,　machine　learning　algorithms　should　be　combined　with　the　traditional　model　checking　approaches　to　improve　the　verification　efficiency　during　train　operation.　In　this　paper,　we　discussed　various　formal　modeling　and　safety　verification　methods　for　the　SRSs　of　TCS　and　pointed　out　the　above　development　directions　for　the　advanced　TCS.　formal　modeling　and　verification　method,　system　requirement　specifications.　©　2024　IEEE.　All　rights　reserved,