In order to satisfy the safety-critical requirements,the train control system(TCS) often employs a layered safety communication protocol to provide reliable services.However,both description and verification of the sa...In order to satisfy the safety-critical requirements,the train control system(TCS) often employs a layered safety communication protocol to provide reliable services.However,both description and verification of the safety protocols may be formidable due to the system complexity.In this paper,interface automata(IA) are used to describe the safety service interface behaviors of safety communication protocol.A formal verification method is proposed to describe the safety communication protocols using IA and translate IA model into PROMELA model so that the protocols can be verified by the model checker SPIN.A case study of using this method to describe and verify a safety communication protocol is included.The verification results illustrate that the proposed method is effective to describe the safety protocols and verify deadlocks,livelocks and several mandatory consistency properties.A prototype of safety protocols is also developed based on the presented formally verifying method.展开更多
The zone control subsystem is a real-time control system,which requests the correctness of the control process.Train tracing scene is an important function of the zone controller(ZC)in the communication based train co...The zone control subsystem is a real-time control system,which requests the correctness of the control process.Train tracing scene is an important function of the zone controller(ZC)in the communication based train control(CBTC)system.In the process of deep development and design,to ensure the safety of the system,the system needs to be modeled,simulated and verified to discover the system design flaws.Unified modeling language(UML)is combined with timed automata,and timed automata network models of train-filter and train tracing demarcation-point are established.At the same time,the verification tool of UPPAAL is applied to simulate the system,and verify the requirements of performance and function of system.The results show that the function of train tracing demaraction-point meets the requirements of system safety and limited activity.Therefore,the method is feasible and can be applied to the modeling and verification of other scenes of train control system.展开更多
As the latest research direction of train-to-train communication,virtual coupling train formation technology has attracted the attention of many scholars.This paper studies the influence of time delay on the formation...As the latest research direction of train-to-train communication,virtual coupling train formation technology has attracted the attention of many scholars.This paper studies the influence of time delay on the formation of virtual coupled trains.We proposed a distributed PID controller,which means that trains can still form a stable fleet operation under the influence of communication delay and control delay.After modelling and analysis,the research uses Matlab to conduct simulation,involving two sets of experiments.Factors including speed,acceleration,position,position error,expected distance between adjacent trains and actual distance between adjacent trains are simulated.The results demonstrate that the distributed PID controller can effectively control the impact of time delay on the virtual coupling fleet.展开更多
基金supported by the New Century Excellent Researcher Award Program from Ministry of Education of China (Grant No. NCET-07-0059)the Fundamental Research Funds for the Central Universities (Grant No.2011YJS006)+1 种基金the National High Technology Research and DevelopmentProgram of China ("863" Program) (Grant No. 2011AA010104)the State Key Laboratory of Rail Traffic Control and Safety Research Project(Grant Nos. RCS2008ZZ001, RCS2008ZZ005)
文摘In order to satisfy the safety-critical requirements,the train control system(TCS) often employs a layered safety communication protocol to provide reliable services.However,both description and verification of the safety protocols may be formidable due to the system complexity.In this paper,interface automata(IA) are used to describe the safety service interface behaviors of safety communication protocol.A formal verification method is proposed to describe the safety communication protocols using IA and translate IA model into PROMELA model so that the protocols can be verified by the model checker SPIN.A case study of using this method to describe and verify a safety communication protocol is included.The verification results illustrate that the proposed method is effective to describe the safety protocols and verify deadlocks,livelocks and several mandatory consistency properties.A prototype of safety protocols is also developed based on the presented formally verifying method.
文摘The zone control subsystem is a real-time control system,which requests the correctness of the control process.Train tracing scene is an important function of the zone controller(ZC)in the communication based train control(CBTC)system.In the process of deep development and design,to ensure the safety of the system,the system needs to be modeled,simulated and verified to discover the system design flaws.Unified modeling language(UML)is combined with timed automata,and timed automata network models of train-filter and train tracing demarcation-point are established.At the same time,the verification tool of UPPAAL is applied to simulate the system,and verify the requirements of performance and function of system.The results show that the function of train tracing demaraction-point meets the requirements of system safety and limited activity.Therefore,the method is feasible and can be applied to the modeling and verification of other scenes of train control system.
文摘As the latest research direction of train-to-train communication,virtual coupling train formation technology has attracted the attention of many scholars.This paper studies the influence of time delay on the formation of virtual coupled trains.We proposed a distributed PID controller,which means that trains can still form a stable fleet operation under the influence of communication delay and control delay.After modelling and analysis,the research uses Matlab to conduct simulation,involving two sets of experiments.Factors including speed,acceleration,position,position error,expected distance between adjacent trains and actual distance between adjacent trains are simulated.The results demonstrate that the distributed PID controller can effectively control the impact of time delay on the virtual coupling fleet.
