基于Prover的联锁软件形式化验证过程研究

• 作者: 张程 王燕芩
• 来源期刊: 铁道通信信号
• 关键词: 联锁软件 形式化验证 模型检验 安全需求
• 年，卷（期）: 2020,（3）
• 所属期刊栏目: 信号·控制
• 页码范围: 17-21
• 页数: 5页
• 字数: 3632字
• 语种: 中文
• DOI: 10.13879/j.issn1000-7458.2020-03.19434

摘要

计算机联锁系统是铁路信号控制系统的核心设备,是有着苛刻安全要求的复杂控制系统.本文采用Prover形式化开发工具对联锁软件安全需求进行形式化验证.通过模型检验的形式化验证方法,遍历系统输入变量的所有状态空间,验证联锁特定应用满足系统安全需求,确保系统的安全性得以正确实现.在保证系统安全性的基础上,以全状态空间查找反例的检验方法进一步提升产品的质量.

作者信息

序号	姓名	单位	发文数	被引次数	H指数	G指数
1	张程		2	1	1.0	1.0
2	王燕芩		4	5	2.0	2.0