|
|||||
|
|
| CTCS-3级列控系统临时限速建模与验证 | |
| 作者姓名： | 袁磊 王俊峰 康仁伟 吕继东 |
| 基金项目： | 国家863计划资助项目(2012AA112801) |
| 摘 要： | 为了满足临时限速系统的实时性要求,采用时间自动机理论,对CTCS-3级列控系统临时限速工作流程分别建立了各设备的时间自动机子模型,进而构成临时限速系统的时间自动机网络模型,并基于临时限速系统技术规范的参数对模型进行赋值;采用BNF语法对临时限速系统待验证的属性进行了形式化描述,并应用UPPAAL验证工具对临时限速模型的安全性和受限活性进行仿真验证.验证结果表明:与现有临时限速系统的时间参数设置相比,修正后的时间参数设置避免了出现系统死锁现象;在不影响安全功能属性和受限活性的基础上,提高了临时限速系统的实时性,可在规范规定时间5 s内做出响应. |
| 关 键 词： | CTCS-3级列控系统 临时限速 时间自动机 UPPAAL 实时性 |
| 收稿时间： | 2012-08-25 |
| 点击此处可从《西南交通大学学报》浏览原始摘要信息 | |
| 点击此处可从《西南交通大学学报》下载全文 | |