计算机联锁系统是铁路信号系统中保证行车安全的重要设备,失效后可能导致重大人员伤亡和财产损失,系统功能逻辑需要具备很高的安全性要求。然而,传统的计算机联锁系统主要采用手工编码的方式进行开发,软件质量主要依赖于代码评审、走查、测试等人工方式进行保障,存在一定的主观性,无法满足计算机联锁系统的高安全性要求。形式化建模是安全关键系统开发的重要方法之一,具有严格的数学基础,能够准确和无歧义地描述系统需求,并且实现逻辑推理,能够有效地解决传统软件开发方法中存在的模糊性和二义性等问题。SCADE是基于形式化建模方法的高安全性软件开发环境,其提供安全状态机和数据流图两种形式化建模方法,能够直观、清晰、全面地描述软件功能逻辑;结合模型仿真和形式化验证能够直观、全面地分析模型的正确性和安全性,避免软件开发人员的主观性;最后自动生成面向工程的高质量的C代码。本文研究基于SCADE的计算机联锁软件开发方法,利用SCADE的需求管理、形式化建模、模型仿真、形式化验证等工具来保证计算机联锁软件的正确性和安全性,具体包括以下内容:(1)介绍了 SCADE的软件开发模式和同步假设理论,并详细分析了 SCADE的需求管理、安全状态机和数据流图建模、模型仿真、形式化验证以及代码生成机制。(2)分析了计算机联锁系统的基本结构、特点及软件功能,根据系统需求将计算机联锁进路控制过程划分为进路选择、进路锁闭、信号开放、信号保持开放、正常通过进路解锁、取消进路六个阶段,分析各阶段中计算机联锁系统SCADE建模的具体需求。(3)采用安全状态机和数据流图两种建模方法,建立计算机联锁系统进路控制过程的形式化模型。(4)利用SCADE需求管理工具分析计算机联锁系统需求、概要设计和形式化模型之间的追溯关系,保证SCADE模型完全覆盖计算机联锁系统的系统需求和概要设计需求。(5)通过图形化的模型仿真,保证计算机联锁软件模型的正确性;然后提取系统安全属性,利用形式化验证检测计算机联锁模型满足预期的安全属性;最后利用代码生成器自动生成面向工程的C代码。