计算机联锁形式化验证典型反例分析  

Analysis of Typical Counterexamples for Formal Verification of Computer Based Interlocking

作　　者：刘丽娟 陈虹 陈耀华 Liu Lijuan;Chen Hong;Chen Yaohua(CASCO Signal Ltd.,Beijing 100070,China)

机构地区：[1]卡斯柯信号有限公司,北京100070

出　　处：《铁路通信信号工程技术》2024年第11期41-45,共5页Railway Signalling & Communication Engineering

基　　金：卡斯柯信号有限公司科研课题项目(RB.1X123015)。

摘　　要：形式化验证是确保计算机联锁系统满足特定安全需求的有效且重要的手段。由于形式化方法的特殊性,要求对于系统模型和安全需求模型的描述完全准确,否则均会导致验证不通过。根据计算机联锁形式化验证的实际经验,总结在安全需求模型建立过程中由于模型建立不完善导致验证失败的典型场景,为形式化验证的实践提供参考。Formal verification is an effective and important means to ensure that the computer based interlocking system can meet specific safety requirements.Due to the particularity of the formal methods,the descriptions of the system model and the safety requirement model need to be completely accurate,failing which the verification will not be passed.Based on the practical experience in the formal verification of the computer based interlocking system,this paper summarizes the typical scenarios of failing to pass the validation when establishing the safety requirement model due to imperfect model establishment,which provides practical reference for formal verification.

关 键 词：形式化验证 计算机联锁 安全需求 反例 

分 类 号：U284.3[交通运输工程—交通信息工程及控制]