Modeling And Verification Of Decentralized Control Interlocking System With Timed Automata

Interlocking system is an essential core technical device of railway signal system,through some technical methods,it contributes to the realization of logic interaction among signal, switch and route belonging to station, so as to ensure the safety of training and improve transportation efficiency.Recently,with the development of controlling technique, communications technology and microelectronics,a new interlocking mode-decentralized control interlocking system has been produced.Decentralized control interlocking system changes the interlocking mode of traditional centralized interlocking.lt distributes the interlock function of host computer by using full electronic module to collect from or drive the field equipment in a form of one-to-one and through intercommunication and collaboration between electronic modules to perform logical computing.Communication and time parameter of the system are vital so that the safe operation of the system must be guaranteed.The current methods to ensure the correctness and safety of interlocking system are simulation,emulation and testing.However,those experimental methods can debug some behaviors of the system, not potential errors. Us ing formalized method to build model for the behaviors of the decentralized control interlocking system can reduce design fault of the interlock system, and this make the problem solved to a certain degree.Firstly,this thesis analyzes and designs the route control process of signal electronic module, switch electronic module and track electronic module based function requirements of decentralized control interlocking system and standard of Computer Interlocking Technology Qualification Based on this, the system communication framework and specific communication process between electronic modules can be obtained.Secondly,this thesis builds the timed automata model for electronic module of beginning signal,conflicting signals witch and track section combined with the Timed Automata Theory.Finally,the timed automata network model of the system route control process is built by checking tool UPPAAL which based on Timed Automata.And through random experiment with simulator, an emulational sequential chart of each module route control process is produced.Communication and state transition of model are also analyzed.Properties of system are extracted through the BNF grammar in the verifier,and then,functionality,time performance and safety of decentralized control interlocking system are verified.