Modeling And Verification Of Interlocking Route Control Process With UPPAAL

Signal system is the main equipment of urban rail transportation,which bears important task to direct train running,ensure running safety and improve the transport efficiency.Computer interlocking(CI) is an important part of signal system.It implements the constraints among signal,switch and route,in order to guarantee the safety of train running.CI in urban rail transportation combine the interlock logic and ATP function together,not only complex in logic,but also increases a lot of special function,it demands higher in safety,reliability and real-time.With the application of computer technology in signal system,the traditional design,analysis and testing methods can not meet the safety requirement of CI.So we adopt a formal method to design and verify interlocking software safely,in order to guarantee the correctness and safety of system design.The paper focuses on route-control process,which is the core of interlocking software in urban rail transportation.The "V" framework is proposed according to the requirements of Safety-Critical System.The paper is wrote based on the general idea of requirements analysis,system design,modeling,formal requirements and formal verification.Firstly,the paper presents base structure and theory of CI software,then analyses function and performance requirements of CI software,on the basis,focuses on route-control process,analyses and designs its main modules and message processing from setting to releasing the route.The method based on Timed Automata is proposed to model route-control process. Sub-automata models of the functional modules and message processing is establish respectively.Finally,establishing timed automata network using UPPAAL.Formal modeling based on Timed Automata describes logic behavior of system using directed graph and real-time performance by the time constraints,thus avoiding inconsistencies, ambiguities and incompleteness in design of interlocking software.Finally,Timed Automata Network of route-control process is simulated and verified in UPPAAL.Formal specification is extracted through the BNF grammar, verifying and analyzing functionality,safety and real-time performance using verifier tools of UPPAAL.The results shows that the formal modeling and verification methods using Timed Automata model and its tools can effectively reduce the fault in system design,provide reference and guidance for design of interlocking software.