CAJ | 학술논문

为了满足铁路线路互联互通以及设备故障之后列车降级运行的需求,列车在运行过程中需要进行等级转换.等级转换过程中,车载设备未正常接收转换预告点、转换执行点应答器的信息,或者列车速度未降至线路允许速度以下等因素,可能导致等级转换不成功,因此有必要通过形式化建模对转换过程分析和验证.本文提出了一种基于UPPAAL的等级转换过程建模与验证方法.采用时间自动机理论建立了CTCS-2/CTCS-3等级转换过程的时间自动机网络模型,应用UPPAAL验证工具对等级转换过程进行仿真分析,验证了等级转换过程的安全性,并对现有技术规范提出了改进意见.
위료만족철로선로호련호통이급설비고장지후열차강급운행적수구,열차재운행과정중수요진행등급전환.등급전환과정중,차재설비미정상접수전환예고점、전환집행점응답기적신식,혹자열차속도미강지선로윤허속도이하등인소,가능도치등급전환불성공,인차유필요통과형식화건모대전환과정분석화험증.본문제출료일충기우UPPAAL적등급전환과정건모여험증방법.채용시간자동궤이론건립료CTCS-2/CTCS-3등급전환과정적시간자동궤망락모형,응용UPPAAL험증공구대등급전환과정진행방진분석,험증료등급전환과정적안전성,병대현유기술규범제출료개진의견.