基于模型的CTCS-3 級列控系統測試案例自動生成方法

呂繼東， 朱曉琳， 李開成， 唐 濤， 王海峰

(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)切換、自動過分相、重聯與摘解、臨時限速、降級情況、調車作……