This　paper　presents　a　parameter　analysis　method　to　solve　the　parameter　uncertainty　problem　for　hybrid　system　and　explore　the　correlation　of　key　parameters　for　distributed　control　system.　For　improving　the　reusability　of　control　model,　the　proposed　approach　provides　the　support　for　obtaining　the　constraint　sets　of　all　uncertain　parameters　in　the　abstract　linear　hybrid　automata　(LHA)　model　when　satisfying　the　safety　requirements　of　the　train　control　system.　Then,　in　order　to　solve　the　state　space　explosion　problem,　the　online　verification　method　is　proposed　to　monitor　the　operating　status　of　high-speed　trains　online　because　of　the　real-time　property　of　the　train　control　system.　Furthermore,　we　construct　the　LHA　formal　models　of　train　tracking　model　and　movement　authority　(MA)　generation　process　as　cases　to　illustrate　the　effectiveness　and　efficiency　of　the　proposed　method.　In　the　first　case,　we　obtain　the　constraint　sets　of　uncertain　parameters　to　avoid　collision　between　trains.　In　the　second　case,　the　correlation　of　position　report　cycle　and　MA　generation　cycle　is　analyzed　under　both　the　normal　and　the　abnormal　condition　influenced　by　packet-loss　factor.　Finally,　considering　stochastic　characterization　of　time　distributions　and　real-time　feature　of　moving　block　control　system,　the　transient　probabilities　of　wireless　communication　process　are　obtained　by　stochastic　time　petri　nets.　(C)　2015　Elsevier　Ltd.　All　rights　reserved.