摘要
CTCS-3级列控系统中的车载设备和RBC之间通过避撞协议进行协调控制。根据列车避撞安全需求,采用安全UML中的安全用例图和安全类图表示避撞协议模型,实现在任意时间间隔内,列车运行速度不超过期望速度,并且列车位置永远不能越过行车许可(MA)的安全功能。避撞协议的安全功能通过连续避撞策略和离散避撞策略的形式化精化实现。前者给出了列车速度和位置为连续变量的情况下,避撞协议的静态结构、动态交互和连续控制策略;后者利用离散逻辑实现了连续避撞策略的离散化。通过对离散避撞策略的进一步精化,生成避撞协议的实时程序代码。严格的形式逻辑WDC*的推理保证了连续避撞策略、离散避撞策略和最终代码精化的正确性和安全性...
-
单位北京交通大学; 电子信息工程学院; 轨道交通控制与安全国家重点实验室