| CTCS-3级列控车载设备的形式化建模与验证 |
| |
| 引用本文： | 何涛,韩敬佳.CTCS-3级列控车载设备的形式化建模与验证[J].重庆大学学报(自然科学版),2023,46(9):120-129. |
| |
| 作者姓名： | 何涛 韩敬佳 |
| |
| 作者单位： | 1.兰州交通大学，自动化与电气工程学院，兰州 730070;2.兰州交通大学，甘肃省工业交通自动化工程技术研究中心，兰州 730070 |
| |
| 基金项目： | 国家自然科学基金资助项目(U2268206)。 |
| |
| 摘 要： | CTCS-3级列控系统安全苛求性较高，而列控车载设备是CTCS-3级列控系统的主体，主要功能是对列车进行操纵和控制，保证列车安全运行的关键。通过分析CTCS-3级列控车载设备之间的信息交互以及车载安全计算机中工作模式的转换规则，采用有色Petri网(CPN)建立车载设备的信息交互模型以及工作模式转换模型，使用ASK-CTL分支时序逻辑公式验证了模型的死标识、死锁以及分析工作模式下的系统行为等特性，验证构建的CPN模型符合系统规范要求的流程及规则，可为相关安全苛求系统的设计提供一定参考。
|
| 关 键 词： | 列控系统 车载设备 模式转换 有色Petri网 |
| 收稿时间： | 2020/6/9 0:00:00 |
Formal modeling and verification of CTCS-3 train control on-board equipment |
| |
| HE Tao,HAN Jingjia.Formal modeling and verification of CTCS-3 train control on-board equipment[J].Journal of Chongqing University(Natural Science Edition),2023,46(9):120-129. |
| |
| Authors: | HE Tao HAN Jingjia |
| |
| Institution: | 1.School of Automation and Electrical Engineering, Lanzhou JiaoTong University, Lanzhou 730070, P. R. China;2.Gansu Research Center of Automation Engineering Technology for Industry &Transportation, Lanzhou JiaoTong University, Lanzhou 730070, P. R. China |
| |
| Abstract: | |
| |
| Keywords: | train control system on-board equipment mode conversion colored Petri net |
|
| 点击此处可从《重庆大学学报(自然科学版)》浏览原始摘要信息 |
| 点击此处可从《重庆大学学报(自然科学版)》下载免费的PDF全文 |
