Abstract: It is necessary to do analysis,verification and test of station interlocking system to ensure the safety of train running and people lives.Especially,the formalized model is the foundation of these works.This paper studied the methodtransforming the sequence diagram(SD) into the event deterministic finite automata(ETDFA) model which is based on UML semi-formal model of computer interlocking software,and used ETDFA as the formal model to describe the system.Firstly,a set of global variables associated with sequence diagram’s interaction were selected as the sate vector to analyze and eliminate the contradiction in pre-value and post-value of message in every scenario and the same message among multiple scenarios,and then based on the sequence event of each object,corresponding ETDFA model was genera-ted.At last,by composing all objects’ ETDFA model,system’s ETDFA formal model was got.The method improves safety software’s designing and development and provides technical support of software quality.

Key words: Computer interlocking software,ETDFA,Sequence diagram,Scenario analysis