摘要
CTCS-3级列控系统中的车载设备和RBC之间通过避撞协议进行协调控制。根据列车避撞安全需求,采用安全UML中的安全用例图和安全类图表示避撞协议模型,实现在任意时间间隔内,列车运行速度不超过期望速度,并且列车位置永远不能越过行车许可(MA)的安全功能。避撞协议的安全功能通过连续避撞策略和离散避撞策略的形式化精化实现。前者给出了列车速度和位置为连续变量的情况下,避撞协议的静态结构、动态交互和连续控制策略;后者利用离散逻辑实现了连续避撞策略的离散化。通过对离散避撞策略的进一步精化,生成避撞协议的实时程序代码。严格的形式逻辑WDC*的推理保证了连续避撞策略、离散避撞策略和最终代码精化的正确性和安全性。
The coordination between the on-board equipment of Chinese Train Control System Level 3 （CTCS-3）and the Radio Block Center（RBC）is realized by the collision avoidance protocol（CAP）.According to the safety requirement for train collision avoidance,the model of CAP is represented by safety use case diagram and safety class diagram in the safety UML to implement the following safety functions：the train speed can never exceed the desired speed in any interval and the train position is never beyond the end of Movement Authority （MA）.The safety function of CAP is implemented by the formal refinement of the continuous and discrete collision avoidance strategies.The former gives the static structure,the dynamic interaction and the continuous control strategy of CAP in the case that the speed and the position of the train are continuous variables.Otherwise,the latter has achieved the discretization for the continuous collision avoidance strategy by discrete logic.The CAP real-time program code is generated through the further refinement of the discrete collision avoidance strategy.The correctness and the safety of the refinement for the continuous and discrete collision avoidance strategies as well as the final code generation have been guaranteed by the rigorous reasoning based on the formal logic-Weakly monotonic time extension of iterative Duration Calculus（WDC＊）.
出处
《中国铁道科学》
EI
CAS
CSCD
北大核心
2010年第6期86-91,共6页
China Railway Science
基金
国家"八六三"计划项目(2009AA11Z221)
国家科技支撑计划项目(2009BAG12A08)
国家自然科学基金资助项目(60634010
60736047)
关键词
列车控制系统
避撞协议
安全UML
避撞策略
Train control system
Collision avoidance protocol
Safety UML
Collision avoidance strategy
