王恪铭 ，王 霞 ，程 鹏 ，刘 宁 ，张传东

（1.西南交通大学信息科学与技术学院，四川 成都 611756；2.西南交通大学系统可信性自动验证国家地方联合工程实验室，四川 成都 610031；3.西南交通大学唐山研究生院，河北 唐山 063000；4.北京和利时系统工程有限公司，北京 100176）

车站联锁系统是典型的安全苛求系统，保障着车站内的行车效率与安全，该系统内在的行为缺陷会对车站的日常运营造成巨大的损失[1].此外，车站联锁系统由联锁表驱动，验证数据的正确性对于该系统的安全运行也至关重要.

形式化方法是提高系统安全可靠性的一种有效方法，当系统的安全完整性等级达到SIL3级及以上时，IEC 61508[2]推荐使用该方法进行系统验证.形式化方法在车站联锁系统中也有应用，如有：文献[3]使用形式化建模工具UPPAAL建立了联锁系统的时间自动机模型，并对安全相关属性进行了验证；文献[4]建立了满足序列释放特性的车站网络联锁系统模型，基于有界模型检验及归纳推理方法，使用SMT（satisfiability modulo theories）求解器进行了验证.

以上研究中都忽略了对联锁数据进行确认，近年来，基于数据视角的系统安全性逐渐被重视，如文献[5]提出了一种用反例引导抽象精化范式的方法对车站联锁数据进行确认，文献[6]中使用ProB证明器确认了联锁数据.

综上所述，目前大多数联锁数据验证研究使用的都是模型检验方法，针对特定对象构建专门的模型.这些方法忽略了不同车站联锁数据确认的通用性.且形式化验证方……