高速列车ATP控车模式的形式化模型与安全性分析

通过评述当前高速列车的发展现状和趋势,结合我国与欧洲在高速列车应用与相关技术研发方面的差距;对ATP控车模式进行分析,并提出采用时段演算针对实时、连续系统的形式化描述工具;根据时段演算的基本符号、公理、定理和推导规则,建立基于时段演算的ATP控车模式形式化模型;通过对模型的推演,对ATP控车模式进行初步安全性分析,发现ATP控车模式下对安全运行发挥主要作用的几个关键环节,特别是确保列车安全行驶,ATP控车与人工控制在转换时应满足的若干时间约束。研究的成果,为设计安全、可靠的ATP系统提供新的理论和分析手段。

Formalization Model of High Speed Trains in ATP Control and Its Safety Analysis

Control of high speed train is the key technique for the safety of train. Through reviewing the state of arts and development trend of high speed train, the difference between China and Europe in the application and technology of high speed train is discussed. The train control pattern in ATP, which will be widely applied in the future, is analyzed. The Duration Calculus, which is a formalization tool aiming at real-time and continuous system, is creatively used to set up the formalization model of train control pattern in ATP based on the notation, axiom, theorem and the rules of deduction of duration calculus. A primary safety analysis of train control pattern in ATP control is given by the inference of the model. Some key factors that play important role in ATP control pattern are found. Especially, time restrictions satisfied during the transition between ATP control and man control are discovered. The achievements provide a new theory analysis method for the design of safe and reliable ATP system.