基于模型的CBTC区域控制系统安全软件开发

Development of Model-based Safety Critical Software for CBTC Zone Control System

传统的软件开发方法不能满足基于通信的列车控制(CBTC)区域控制系统(ZC)的开发需求。结合北京地铁亦庄线研究项目,介绍一种基于模型的系统开发方法,给出ZC系统的软件容错结构,阐述该系统的移动授权和列车管理功能建模方法,并从模型覆盖率分析和形式化验证两方面深入分析系统安全性保障措施。ZC系统的研究项目表明,基于模型的开发方法能够更好地保证系统的开发质量和安全性。

Traditional software development methods cannot meet the challenges of the development of CBTC Zone Control system（ZC）.Based on engineering practice of Beijing Yizhuang metro line,this paper introduces a model-based development approach.The fault-tolerant architecture of ZC system is presented and the function modeling methods of moving authority and train management are introduced.The model test coverage analysis and formal verification for the safety of ZC model are further explored.Engineering practice of ZC system shows that the model-based development approach is helpful for ensuring the quality and safety of the system.