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

Method for Verifying the Correctness of Train Control System Design

作　　者：曹源[1] 唐涛[1] 罗丹[2] 穆建成 

机构地区：[1]北京交通大学轨道交通控制与安全国家重点实验室,北京100044 [2]北京二七轨道交通装备有限责任公司科研管理部北京100072 [3]铁道部科学技术司,北京100844

出　　处：《西南交通大学学报》2010年第4期574-579,共6页Journal of Southwest Jiaotong University

基　　金：国家自然科学基金重点资助项目(60634010和60736047);国家科技计划支撑项目(2009BAG12A08);高等学校博士学科点专项科研基金资助项目(20070004005);轨道交通控制与安全国家重点实验室自主研究课题(RCS2008ZZ005);北京市轨道交通控制重点实验室

摘　　要：为验证系统开发阶段列车运行控制系统设计的正确性,提出了基于RAISE软件的系统建模、描述及验证方法.以CTCS-3级两列列车追踪运行为例,采用面向系统特性的域,建立了系统域模型,并在对域模型扩充和完善的基础上,用RSL语言描述了两列列车追踪运行情况.根据RSL语言描述的公理及RAISE自身的推理规则,验证了当两列列车追踪运行时,CTCS-3级列车运行控制系统设计的正确性.To verify the correctness of a train control system design in the development stage,a formal method,which is based on RAISE（rigorous approach to industrial software engineering） and can be used for system modeling,description and verification,was proposed.For the tracking operation between two trains of CTCS-3（China train control system level 3）,domain models of the system were established by adopting feature-oriented domains.After extending and improving the domain models using RAISE specification language（RSL）,a final description of the tracking operation between two trains was formed.With the axioms described by RSL and reasoning rules of RAISE,the system design of CTCS-3 was verified correct in the context of tracking scene between two trains.

关 键 词：交通信息工程 形式化方法 列车运行控制系统 安全苛求系统 

分 类 号：U283.2[交通运输工程—交通信息工程及控制]