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

Development of CBTC System Safety Software Based on Formalization Method

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

A formalization method for safety related software development in CBTC system is presented,including formal description of software requirement,software formalized modeling,and software formalized verification.The author illustrates the application of this method in the development of generic application software of the zone controller of TRANAVI CBTC system as an example of safety critical system.It is shown that this method can avoid many problems of traditional method such as ambiguous requirement description,inconsistent between requirement and design and it can help to improve the quality of software and reduce the risk at late period of aproject.