王 鲲

(1.中国铁道科学研究院 通信信号研究所，北京 100081；2.国家铁路智能运输系统工程技术研究中心，北京 100081)

在基于通信的列车控制(Communication Based Train Control，CBTC)系统中，计算机联锁系统(简称CBTC联锁系统)是重要的基础设备之一。随着CBTC技术日趋精密复杂，CBTC联锁系统不仅需要通过复杂的逻辑状态运算以实现对联锁进路、信号机、道岔、轨道区段、站台门、防淹门等的控制，还需要与外部系统进行实时通信，实现数据交互，而且在进行逻辑计算时涉及巨大的内部状态空间，在与外部系统实时通信时引入了大量的并发性和不确定性，因此该系统是一种典型的复杂安全苛求系统。同时，CBTC联锁系统的关键性质与其功能性混合在一起，并与软件开发的全过程密切相关，使得这些关键性质的获得和保证变得更加复杂。因此，如何在CBTC联锁系统软件的开发和维护中保证软件具有所需的安全性、无死锁性等关键性质，成为了重要的研究方向。

统计表明，传统的非形式化的软件工程技术对软件质量的保证具有一个难以逾越的顶点，而形式化方法的实践证明形式化方法是提高软件质量的重要途径[1]。形式化的方法通过严格的数学方法，定性定量地描述软件的行为，建立关键性质与软件行为之间的内在联系和严格描述，从而设计并验证软件所需的关键性质。标准IEC62279：2002《铁路应用：通信、信号、处理系统——铁路控制和防护系统软件》[2]中指出：“在软件安全完善度等级为4级时，软件需求规格说明书定义、软件设计和实施、验证和测试等过程中，强力推荐使用形式化方法进行描述和设计；……