列车运行控制系统设计正确性的验证方法

详细信息   全文下载|推荐本文 |

• 出版年：2010
• 作者：曹源；唐涛；罗丹；穆建成
• 单位1：北京交通大学轨道交通控制与安全国家重点实验室
• 出生年：1982
• 学历：博士研究生
• 语种：中文
• 作者关键词：交通信息工程；形式化方法；列车运行控制系统；安全苛求系统
• 起始页：574
• 总页数：6
• 经费资助：国家自然科学基金重点资助项目（60634010和60736047）；国家科技计划支撑项目（2009BAG12A08）；高等学校博士学科点专项科研基金资助项目（20070004005）
• 刊名：西南交通大学学报
• 是否内版：否
• 刊频：双月刊
• 创刊时间：1954
• 主管单位：中华人民共和国教育部
• 主办单位：西南交通大学
• 主编：翟婉明
• 地址：中国、成都
• 邮编：610031
• 电子信箱：xbz@home.swjtu.edu.cn
• 网址：http://journal.swjtu.edu.cn
• 卷：45
• 期：4
• 期刊索取号：P860.6 210
• 数据库收录：EI Compendex收录期刊；中文核心期刊；中国科技论文统计源期刊；中国科学引文数据库来源期刊；德国数学文摘（Zbl MATH)收录期刊
• 核心期刊：中文核心期刊

摘要

为验证系统开发阶段列车运行控制系统设计的正确性，提出了基于RAISE软件的系统建模、描述及验证方法.以CTCS-3级两列列车追踪运行为例，采用面向系统特性的域，建立了系统域模型，并在对域模型扩充和完善的基础上，用RSL语言描述了两列列车追踪运行情况.根据RSL语言描述的公理及RAISE自身的推理规则，验证了当两列列车追踪运行时，CTCS-3级列车运行控制系统设计的正确性.