应用技术领域：轨道交通控制系统

负责人：计算机学院陈祖希
成果简介：

为提高列车安全控制系统的安全性、可靠性，提升安全苛刻相关软件研发质量，卡斯柯信号有限公司委托华侨大学在安全苛刻软件的形式化验证、测试方面展开研究。本技术条款约定双方合作的首阶段相关工作，相关要求如下：
研究采用形式化方法对联锁安全需求通过基于Event-B的技术进行验证：

1)针对甲方联锁系统安全需求验证需求，乙方研究可行的形式化验证方法；

2)通过基于Event-B的技术乙方建立联锁安全需求模型示例，完成对联锁需求安全模型的形式化验证；

3)通过基于Event-B的技术乙方提供形式化建模与验证的方案及理论基础，并展示证明过程与最终的证明结果。