论文部分内容阅读
CTCS-3级列控系统中的车载设备和RBC之间通过避撞协议进行协调控制。根据列车避撞安全需求,采用安全UML中的安全用例图和安全类图表示避撞协议模型,实现在任意时间间隔内,列车运行速度不超过期望速度,并且列车位置永远不能越过行车许可(MA)的安全功能。避撞协议的安全功能通过连续避撞策略和离散避撞策略的形式化精化实现。前者给出了列车速度和位置为连续变量的情况下,避撞协议的静态结构、动态交互和连续控制策略;后者利用离散逻辑实现了连续避撞策略的离散化。通过对离散避撞策略的进一步精化,生成避撞协议的实时程序代码。严格的形式逻辑WDC*的推理保证了连续避撞策略、离散避撞策略和最终代码精化的正确性和安全性。
CTCS-3 train control system in-vehicle equipment and RBC through the collision avoidance protocol for coordinated control. According to the safety requirements of the train collision avoidance, the safety case diagram and safety class diagram of the safety UML are used to represent the collision avoidance protocol model so that the train running speed does not exceed the expected speed at any time interval and the train position can never exceed the driving permission (MA ) Security features. The security features of the collision avoidance protocol are formalized by the continuous collision avoidance strategy and the discrete collision avoidance strategy. The former gives the static structure of the collision avoidance protocol, dynamic interaction and continuous control strategy when the train speed and position are continuous variables. The latter uses the discrete logic to realize the discretization of continuous collision avoidance strategy. Through the further refinement of discrete collision avoidance strategy, real-time code generated collision avoidance protocol. Strict formal logic The reasoning of WDC * ensures the correctness and safety of continuous avoidance strategies, discrete collision avoidance strategies, and final code refinement.