基于模型检验的计算机联锁软件验证方法  

Model-based Verification Method of Computer Interlocking Software

作　　者：刘丽娟 Liu Lijuan

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

出　　处：《铁道通信信号》2020年第8期35-38,共4页Railway Signalling & Communication

摘　　要：采用形式化验证是确认计算机联锁软件能够满足特定安全属性的一种有效手段.本文描述了一种基于模型检验的方法,对联锁系统模型及安全属性模型的建立方法进行探讨,并结合具体的站场实例,对信号开放功能进行了模型描述和验证,结果表明该方法用于计算机联锁系统具备可行性.Formal verification is an effective means to verify whether the software of the comput.er interlocking system can satisfy specific safety requirements.So,a model-based verification method is described and the modeling of the interlocking system as well as its safety requirement specification is discussed.And in the case of a specific railway yard.the function of clearing of signal is described with the model and verified.The results indicate that this method is applicable for the interlocking system.

关 键 词：计算机联锁 形式化验证 模型检验 

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