基于形式化方法的CBTC系统安全软件开发

提出了一套适用于城市轨道交通CBTC系统安全软件开发的形式化方法,包括软件需求形式化描述、软件形式化建模和软件设计形式化验证。以TRANAVI型CBTC系统区域控制器(ZC)通用应用软件为例,说明该套方法在安全苛求系统开发中的应用。实践证明:该方法可以有效避免传统开发方法中由于需求定义不精确、需求/设计不一致等造成的软件失效问题,对于提升安全软件开发质量,降低项目后期风险有很大帮助。