Abstract: It is an important way to make sure the safety of train running and passengers’ life and property by effectively testing,analyzing and validating computer interlocking software．Formal model is the foundation of system testing,analyzing and validating．Based on interlocking software’s UML informal model,using finite state machine model as the mathematical tools to describe system formal model,this paper studied the method to traverse the UML sequence diagram or scenarios to finite state machine model．Firstly the UML sequence diagram was traversed to FSP process ma-thematical model,and then systematic finite state machine model was obtained by merging all objects’ process mathematic models in the UML sequence diagram．Finally,the case of controlling of entry routes was used to generate systematic finite state machine model to invalidate the feasibility and effectiveness of this method.

Key words: Interlocking software,UML,Sequence diagram,FSP,Finite process machine