摘要
特定车站的联锁安全软件因其变量复杂且变量间耦合众多,使得传统测试很难覆盖所有的联锁场景,而形式化验证具有遍历系统各个状态的特点,可以实现联锁所有可能场景的验证。研究了联锁安全软件的形式化验证流程,包括安全需求的提炼、形式化表述,以及安全需求的实例化和验证;通过2组案例分析验证了该流程的有效性。
Due to the interlocking safety software of a specific station has complex variables and many coupling variables,it is difficult for the traditional test to cover all interlocking scenarios,while the formal verification has the characteristics of traversing all states of the system,which can realize the verification of all possible interlocking scenarios.Therefore,a formal verification process for interlocking safety software is discussed in this study.The specific steps of the method include the refining and formal expression of safety requirements,as well as the instantiation and verification of safety requirements.The effectiveness of this process is verified through two groups of case studies.
作者
魏民
刘晓
张文燕
王燕芩
Wei Min;Liu Xiao;Zhang Wenyan;Wang Yanqin
出处
《铁道通信信号》
2022年第12期28-31,共4页
Railway Signalling & Communication
关键词
特定车站
联锁系统
危害分析
形式化验证
模型检测
Specific railway station
Interlocking system
Hazard analysis
Formal verification
Model checking
