Abstract: To meet the needs of high safety of automatic train protection system, this paper proposed and implemented an optimized UML-based rectuirement modeling method. By learning from the formal method, this paper improved the classical state machine model, and introduced a super-state machine with a series of accurate pre-defined rules, to implement the formal modeling of ATP system. Applied the method to an urban rail transit signal system, the result shows that the model established in this paper reduces the software failure by avoiding the ambiguity, meanwhile, it greatly improves the safety and reliability and makes the system more easily to develop and maintain.

Key words: Automatic train protection,Requirement modeling,UML,Formal method,Safety