ETCS-2级列车运行控制系统呈现复杂的混成性.按照无线闭塞中心(RBC)交接协议的内容,建立RBC交接协议的UML图；基于微分动态逻辑理论,从混成系统角度对ETCS-2级列控系统规范中的RBC交接协议进行建模.建立的RBC交接协议模型包括列车子模型、移交子模型和接收子模型.根据模型的性质,构造微分不变式,运用证明工具KeYmaera验证模型的安全性和活性.结合专业知识对关键性的约束条件进行分析并将其反馈至模型,实现模型的精化.在模型验证过程中,发现了交接安全及交接效率的参数约束条件,由此参数约束条件可知,RBC交接效率受RBC离散控制时间和列车运行状况的共同影响.%ETCS-2 presents the characteristics of complex hybrid. According to the handover protocol of Radio Block Center (RBC), the UML diagram of RBC handover protocol is given. Modeling is carried through on the RBC handover protocol in ETCS-2 train control system specification from the point of hybrid system based on differential dynamic logic. The established model of RBC handover protocol consists of train submodel, handover submodel and takeover submodel. According to model characteristics, differential invariants are structured and proved by KeYmaera to validate the safety and liveness of the model. Combining with the domain knowledge, the key constraints are analyzed and fed back to the initial model in order to refine the model. During model validation process, the constraints for handover safety and efficiency parameters are found. It's known from parameter constraints that RBC handover efficiency is influenced by both the discrete control time of RBC and the running state of the train.
展开▼
