摘要
为验证系统开发阶段列车运行控制系统设计的正确性,提出了基于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.
出处
《西南交通大学学报》
EI
CSCD
北大核心
2010年第4期574-579,共6页
Journal of Southwest Jiaotong University
基金
国家自然科学基金重点资助项目(60634010和60736047)
国家科技计划支撑项目(2009BAG12A08)
高等学校博士学科点专项科研基金资助项目(20070004005)
轨道交通控制与安全国家重点实验室自主研究课题(RCS2008ZZ005)
北京市轨道交通控制重点实验室
