车站联锁系统行为验证与数据确认的形式化方法  

Formal Method for Behavior Verification and Data Validation of Station Interlocking System

作　　者：王恪铭 王霞[1,2] 程鹏 刘宁[2,3] 张传东[4] WANG Keming;WANG Xia;CHENG Peng;LIU Ning;ZHANG Chuandong(School of Information Science and Technology,Southwest Jiaotong University,Chengdu 611756,China;National-Local Joint Engineering Laboratory of System Credibility Automatic Verification,Southwest Jiaotong University,Chengdu 610031,China;Graduate School of Tangshan,Southwest Jiaotong University,Tangshan 063000,China;Beijing HollySys Co.,Ltd.,Beijing 100176,China)

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

出　　处：《西南交通大学学报》2021年第3期587-593,610,共8页Journal of Southwest Jiaotong University

基　　金：国家自然科学基金(71502146,61673320);中央高校基本科研业务费专项资金(2682017ZT12)。

摘　　要：车站联锁系统是一种典型的基于数据驱动的安全苛求系统,开发过程中需要对系统行为进行验证并需确认数据的正确性.为此,通过分析联锁系统的设计规范,基于RODIN平台并使用Event-B语言,辅助使用UML(unified modeling language)图工具快速建立系统的初始模型,以自动生成模型文件并描述出各系统属性与事件流程;基于精化策略分层建模,对各层模型的证明义务进行定理证明,验证了系统的各项属性,得出可靠的通用功能模型;基于实例车站,对模型的公理进行了验证,同时实现了对联锁数据的确认;通过形式化验证过程,结合给定场景联锁数据的有效性确认,发现并纠正系统需求及分析过程中造成的潜在行为缺陷;通过功能仿真与验收测试,进一步确认了通用模型与联锁数据的正确性.结果表明:本文方法提高了基于模型开发过程的准确性与层次性,验证了系统通用行为状态,且结合公理验证,实现了联锁数据的确认,并能基于模型进行功能场景仿真与测试,从而可进一步提高系统通用功能原型的可靠性.Station interlocking system is a typical safety-critical system driven by data,which needs to verify the system behavior and confirm the correctness of data in the development.After analyzing the design specifications of the interlocking system,the initial system model was built automatically by the UML(unified modeling language)diagram,with the system properties and event flows described by Event-B language on RODIN platform.Subsequently,the refinement policy was used for hierarchical modeling,and the proof obligations of each layer were proved by theorem and the properties of the system attributions were verified.Thus,a reliable universal function model was obtained.Using a real station yard,the axioms of the model were proved and the interlocking data were validated as well.According to the formal verification and data validation in a given scenario,the subtle defects generated in the analysis of the system requirements could be found and corrected.Finally,the functional simulation and acceptance testing confirmed the correctness of the general model and the interlock data.This method not only improves the accuracy and hierarchy of the model-based development,but also verifies the universal behavior state of the system.Combined with axiomatic verification,the validation of interlocking data is realized.The function scenario can be simulated and tested based on the model,which can further improve the reliability of the universal function prototype of the system.

关 键 词：车站联锁系统 形式化验证 定理证明 数据确认 功能仿真 测试 

分 类 号：TP301.1[自动化与计算机技术—计算机系统结构] U284.3[自动化与计算机技术—计算机科学与技术]