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

作者：曹源; 唐涛; 罗丹; 穆建成

来源：西南交通大学学报, 2010, (04): 574-579.

• 交通信息工程
• 形式化方法
• 列车运行控制系统
• 安全苛求系统 traffic information engineering
• formal method
• train control system
• safe critical system

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

• 单位
  北京交通大学; 轨道交通控制与安全国家重点实验室