CTCS-3级列控系统避撞协议的建模、设计和实现
CTCS-3级列控系统中的车载设备和RBC之间通过避撞协议进行协调控制.根据列车避撞安全需求,采用安全UML中的安全用例图和安全类图表示避撞协议模型,实现在任意时间间隔内,列车运行速度不超过期望速度,并且列车位置永远不能越过行车许可(MA)的安全功能.避撞协议的安全功能通过连续避撞策略和离散避撞策略的形式化精化实现.的者给出了列车速度和位置为连续变量的情况下,避撞协议的静态结构、动态交互和连续控制策略;后者利用离散逻辑实现了连续避撞策略的离散化.通过对离散避撞策略的进一步精化,生成避撞协议的实时程序代码.严格的形式逻辑WDC*的推理保证了连续避撞策略、离散避撞策略和最终代码精化的正确性和安全性.
列车控制系统、避撞协议、安全UML、避撞策略
31
U284.482(铁路通信、信号)
国家高技术研究发展计划(863计划);国家科技支撑计划;国家自然科学基金
2011-03-07(万方平台首次上网日期,不代表论文的发表时间)
共6页
86-91