吕继东， 朱晓琳， 李开成， 唐 涛， 王海峰

(1. 北京交通大学轨道交通运行控制系统国家工程研究中心，北京100044;2. 中国铁道科学研究院通信信号研究所，北京100044;3. 北京交通大学轨道交通控制与安全国家重点实验室，北京100044)

作为典型的安全苛求系统，列控系统功能的任何故障都可能造成巨大的生命和财产损失［1］. 形式化方法和测试方法是保证列控系统功能正确性的两个重要途径，在列控系统开发生命周期中起着不同的作用.

形式化方法一般用于列控系统开发的前期，已广泛用于列控系统需求规范的功能正确性研究［2］.早期列控系统的形式化研究主要使用时段演算方法(duration calculus，DC)［3］. 然而，时段演算不能完全满足列控系统的形式化建模要求，随着列控系统复杂度的提高，系统中诸如期限(deadline)、直到…才(wait until)、超时(time out)等形式化描述存在一 定 的 不足［4］. 进程代 数(process algebra)通过描述并发和通信系统为分析离散事件系统提供了结构化方法［5］，其中，HCSP(hybrid communication sequential process)方法是对CSP(communication sequential process)的一种扩展，广泛应用于列控系统功能正确性研究［6］. 一致性测试是保证系统功能正确性的另一个重要手段，一般用于列控系统开发的后期.通过分析被测系统(system under test，SUT)与其需求规范之间的关系，验证系统的功能是否与需求规范一致［7］. 国内外列控系统功能一致性测试的研究主要集中在测试案例生成方法上［8-10］.

CTCS-3 级列控系统功能复杂，涵盖了注册与启动、注销、等级转换、行车许可、RBC(radio block center)切换、自动过分相、重联与摘解、临时限速、降级情况、调车作……