CAJ | 학술논문

在CTCS-3(Chinese Train Control System Level 3)级列控系统中,RBC(Radio Block Center)切换是影响列车安全高效运行的重要环节,现阶段对RBC切换协议进行验证分析所使用的形式化方法还存在状态爆炸或描述性质单一等问题。基于Timed RAISE的形式化方法,结合域的模型,在对RBC切换流程分析的基础上,构建状态转移图,得到切换协议的形式化模型,使用等价和推断的推理规则对模型的正确性和实时性进行推理验证,得到的结果表明,RBC切换协议满足规范标准对正确性与实时性的要求,将验证结果与其他文献的结论进行比较分析,说明该方法具有通用性,对于推广其在列控系统场景验证中的应用有一定的实际意义。
재CTCS-3(Chinese Train Control System Level 3)급렬공계통중,RBC(Radio Block Center)절환시영향열차안전고효운행적중요배절,현계단대RBC절환협의진행험증분석소사용적형식화방법환존재상태폭작혹묘술성질단일등문제。기우Timed RAISE적형식화방법,결합역적모형,재대RBC절환류정분석적기출상,구건상태전이도,득도절환협의적형식화모형,사용등개화추단적추리규칙대모형적정학성화실시성진행추리험증,득도적결과표명,RBC절환협의만족규범표준대정학성여실시성적요구,장험증결과여기타문헌적결론진행비교분석,설명해방법구유통용성,대우추엄기재렬공계통장경험증중적응용유일정적실제의의。
In the CTCS-3-based train control system, the Radio Block Center ( RBC ) handover is an important part closely related to train safety and efficiency. The formal methods used for verifying and analyzing train control system tend to have some problems such as state explosion and singularity of description. Based on the analysis of RBC handover, the Domain method merging with Timed RAISE formal is applied to construct state transition diagram and obtain the formal model of handover protocol, and the inference rules are used to verify the correctness and real time of handover protocol. The result shows that the protocol satisfies the requirements for correctness and real time. The verification results are compared with other literatures and proved to be suitable for scene verification in train control system.